1	import Base
2	import ../../lib/logic.bend as L
3	import ../../../spec/lib/common.bend as SC
4	import ../../../src/math/pow2.bend as P
5	
6	# The tail-recursive 2^d (src/pow2.bend) is the structural spec pow2.
7	
8	def go_double(+d: Nat, +acc: Nat) -> {P.go(d, Nat.double(acc)) == Nat.double(P.go(d, acc)) : Nat}:
9	  match d:
10	    case 0n:
11	      {==}
12	    case 1n+ +p:
13	      go_double(p, Nat.double(acc))
14	
15	def same(+d: Nat) -> {P.pow2t(d) == SC.pow2(d) : Nat}:
16	  match d:
17	    case 0n:
18	      {==}
19	    case 1n+ +p:
20	      Equal.trans(Nat, P.go(p, 2n), Nat.double(P.go(p, 1n)), SC.pow2(1n+p), go_double(p, 1n), Equal.cong(Nat, Nat, Nat.double, P.go(p, 1n), SC.pow2(p), same(p)))