1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bitsv.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../../spec/crypto/secp256k1/field.bend as FS
5	import ../../../src/crypto/secp256k1/limbs.bend as L
6	import ../../lib/nat.bend as N
7	import ../../lib/logic.bend as Lg
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../math/natural/arith.bend as NR
10	import ../../math/typed/width.bend as WW
11	import ./semiring.bend as SR
12	import ./limbs.bend as LV
13	import ./ineq.bend as I
14	import ./reduce.bend as R
15	
16	# The bits of limb lists (src/crypto/secp256k1/limbs.bend bits, bits_of,
17	# cbits) and the number they spell, most significant first, with every
18	# bit worth `one` (hv), so that a 256-bit exponent stays symbolic.
19	
20	def hv(bs: List<&2, Nat>, +one: Nat, +e: Nat) -> Nat:
21	  match bs:
22	    case Nil{}: e
23	    case b <> t: hv(t, one, Nat.add(Nat.mul(b, one), Nat.double(e)))
24	
25	def hv_app(+one: Nat, xs: List<&2, Nat>, +e: Nat, +ys: List<&2, Nat>) -> {hv(List.append(&2, Nat, xs, ys), one, e) == hv(ys, one, hv(xs, one, e)) : Nat}:
26	  match xs:
27	    case Nil{}:
28	      {==}
29	    case +x <> +t:
30	      hv_app(one, t, Nat.add(Nat.mul(x, one), Nat.double(e)), ys)
31	
32	def all01(bs: List<&2, Nat>) -> Bool:
33	  match bs:
34	    case Nil{}: True{}
35	    case b <> t: Bool.and(Nat.is_lt(b, 2n), all01(t))
36	
37	def all01_app(xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {all01(xs) == True{} : Bool}, +hy: {all01(ys) == True{} : Bool}) -> {all01(List.append(&2, Nat, xs, ys)) == True{} : Bool}:
38	  match xs:
39	    case Nil{}:
40	      hy
41	    case +x <> +t:
42	      Lg.and_intro(Nat.is_lt(x, 2n), all01(List.append(&2, Nat, t, ys)), Lg.and_left(Nat.is_lt(x, 2n), all01(t), hx), all01_app(t, ys, Lg.and_right(Nat.is_lt(x, 2n), all01(t), hx), hy))
43	
44	def mod2_lt(+x: Nat) -> {Nat.is_lt(Nat.mod(x, 2n), 2n) == True{} : Bool}:
45	  NR.dm_lt(1n, x)
46	
47	def bits_of01(k: Nat, +x: Nat) -> {all01(L.bits_of(k, x)) == True{} : Bool}:
48	  match k:
49	    case 0n:
50	      {==}
51	    case 1n+ +j:
52	      all01_app(L.bits_of(j, Nat.div(x, 2n)), [Nat.mod(x, 2n)], bits_of01(j, Nat.div(x, 2n)), Lg.and_intro(Nat.is_lt(Nat.mod(x, 2n), 2n), True{}, mod2_lt(x), {==}))
53	
54	def bits01(xs: List<&2, Nat>) -> {all01(L.bits(xs)) == True{} : Bool}:
55	  match xs:
56	    case Nil{}:
57	      {==}
58	    case +x <> +t:
59	      all01_app(L.bits(t), L.bits_of(16n, x), bits01(t), bits_of01(16n, x))
60	
61	# ---- the value of bits_of ----
62	
63	# d < 2 s gives d / 2 < s
64	def two_x(+x: Nat) -> {Nat.mul(x, 2n) == Nat.add(x, x) : Nat}:
65	  %Equal.sym(Nat, Nat.mul(x, 2n), Nat.mul(2n, x), NA.mul_comm(x, 2n)) : {_ == Nat.add(x, x) : Nat}
66	  %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {Nat.add(x, _) == Nat.add(x, x) : Nat}
67	  {==}
68	
69	def half_lt(+d: Nat, +s: Nat, +h: {Nat.is_lt(d, Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(d, 2n), s) == True{} : Bool}:
70	  +q = Nat.div(d, 2n)
71	  +le = I.le_subst_r(Nat.mul(q, 2n), Nat.add(Nat.mul(q, 2n), Nat.mod(d, 2n)), d, Equal.sym(Nat, d, Nat.add(Nat.mul(q, 2n), Nat.mod(d, 2n)), NR.dm_eq(1n, d)), N.le_add_right(Nat.mul(q, 2n), Nat.mod(d, 2n)))
72	  +e2 = Equal.trans(Nat, Nat.double(s), Nat.add(s, s), Nat.mul(s, 2n), NA.double_self(s), Equal.sym(Nat, Nat.mul(s, 2n), Nat.add(s, s), two_x(s)))
73	  R.mul_lt_cancel(2n, q, s, N.le_lt_trans(Nat.mul(q, 2n), d, Nat.mul(s, 2n), le, I.lt_subst_r(d, Nat.double(s), Nat.mul(s, 2n), e2, h)), Nat.is_lt(q, s), {==})
74	
75	# the k bits of d < 2^k spell d
76	def bits_of_v(+one: Nat, +h1: {one == 1n : Nat}, k: Nat, +d: Nat, +e: Nat, +hd: {Nat.is_lt(d, C.shift(k, one)) == True{} : Bool}) -> {hv(L.bits_of(k, d), one, e) == Nat.add(C.shift(k, e), Nat.mul(one, d)) : Nat}:
77	  match k:
78	    case 0n:
79	      +d0 = N.lt_succ_le(d, 0n, I.lt_subst_r(d, one, 1n, h1, hd))
80	      +ez = N.le_antisym(d, 0n, d0, N.zero_le(d))
81	      %Equal.sym(Nat, d, 0n, ez) : {e == Nat.add(e, Nat.mul(one, _)) : Nat}
82	      %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {e == Nat.add(e, _) : Nat}
83	      %Equal.sym(Nat, Nat.add(e, 0n), e, NA.add_zero(e)) : {e == _ : Nat}
84	      {==}
85	    case 1n+ +j:
86	      +q = Nat.div(d, 2n)
87	      +r = Nat.mod(d, 2n)
88	      %Equal.sym(Nat, hv(List.append(&2, Nat, L.bits_of(j, Nat.div(d, 2n)), [Nat.mod(d, 2n)]), one, e), hv([Nat.mod(d, 2n)], one, hv(L.bits_of(j, Nat.div(d, 2n)), one, e)), hv_app(one, L.bits_of(j, Nat.div(d, 2n)), e, [Nat.mod(d, 2n)])) : {_ == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, d)) : Nat}
89	      %Equal.sym(Nat, hv(L.bits_of(j, Nat.div(d, 2n)), one, e), Nat.add(C.shift(j, e), Nat.mul(one, Nat.div(d, 2n))), bits_of_v(one, h1, j, Nat.div(d, 2n), e, half_lt(d, C.shift(j, one), hd))) : {hv([Nat.mod(d, 2n)], one, _) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, d)) : Nat}
90	      %Equal.sym(Nat, d, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)), NR.dm_eq(1n, d)) : {Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.double(Nat.add(C.shift(j, e), Nat.mul(one, Nat.div(d, 2n))))) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, _)) : Nat}
91	      %Equal.sym(Nat, Nat.mul(one, Nat.div(d, 2n)), Nat.mul(Nat.div(d, 2n), one), NA.mul_comm(one, Nat.div(d, 2n))) : {Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.double(Nat.add(C.shift(j, e), _))) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
92	      %Equal.sym(Nat, Nat.double(Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one))), Nat.add(Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one)), Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one))), NA.double_self(Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one)))) : {Nat.add(Nat.mul(Nat.mod(d, 2n), one), _) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
93	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one)), Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one))), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one)))), NA.add_assoc(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one), Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one)))) : {Nat.add(Nat.mul(Nat.mod(d, 2n), one), _) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
94	      %Equal.sym(Nat, Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(C.shift(j, e), Nat.mul(Nat.div(d, 2n), one))), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))), NA.add_swap(Nat.mul(Nat.div(d, 2n), one), C.shift(j, e), Nat.mul(Nat.div(d, 2n), one))) : {Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.add(C.shift(j, e), _)) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
95	      %Equal.sym(Nat, Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))))), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))))), NA.add_swap(Nat.mul(Nat.mod(d, 2n), one), C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))))) : {_ == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
96	      %Equal.sym(Nat, Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one)))), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one)))), NA.add_swap(Nat.mul(Nat.mod(d, 2n), one), C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one)))) : {Nat.add(C.shift(j, e), _) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
97	      %Equal.sym(Nat, Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))), NA.add_swap(Nat.mul(Nat.mod(d, 2n), one), Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), _)) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
98	      %Equal.sym(Nat, Nat.add(Nat.mul(Nat.mod(d, 2n), one), Nat.mul(Nat.div(d, 2n), one)), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one)), NA.add_comm(Nat.mul(Nat.mod(d, 2n), one), Nat.mul(Nat.div(d, 2n), one))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), _))) == Nat.add(Nat.double(C.shift(j, e)), Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
99	      %Equal.sym(Nat, Nat.double(C.shift(j, e)), Nat.add(C.shift(j, e), C.shift(j, e)), NA.double_self(C.shift(j, e))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(_, Nat.mul(one, Nat.add(Nat.mul(Nat.div(d, 2n), 2n), Nat.mod(d, 2n)))) : Nat}
100	      %Equal.sym(Nat, Nat.mul(Nat.div(d, 2n), 2n), Nat.add(Nat.div(d, 2n), Nat.mul(Nat.div(d, 2n), 1n)), NA.mul_succ(Nat.div(d, 2n), 1n)) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.mul(one, Nat.add(_, Nat.mod(d, 2n)))) : Nat}
101	      %Equal.sym(Nat, Nat.mul(Nat.div(d, 2n), 1n), Nat.div(d, 2n), NA.mul_one(Nat.div(d, 2n))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.mul(one, Nat.add(Nat.add(Nat.div(d, 2n), _), Nat.mod(d, 2n)))) : Nat}
102	      %Equal.sym(Nat, Nat.add(Nat.add(Nat.div(d, 2n), Nat.div(d, 2n)), Nat.mod(d, 2n)), Nat.add(Nat.div(d, 2n), Nat.add(Nat.div(d, 2n), Nat.mod(d, 2n))), NA.add_assoc(Nat.div(d, 2n), Nat.div(d, 2n), Nat.mod(d, 2n))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.mul(one, _)) : Nat}
103	      %Equal.sym(Nat, Nat.mul(one, Nat.add(Nat.div(d, 2n), Nat.add(Nat.div(d, 2n), Nat.mod(d, 2n)))), Nat.add(Nat.mul(one, Nat.div(d, 2n)), Nat.mul(one, Nat.add(Nat.div(d, 2n), Nat.mod(d, 2n)))), NA.mul_add_left(one, Nat.div(d, 2n), Nat.add(Nat.div(d, 2n), Nat.mod(d, 2n)))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), _) : Nat}
104	      %Equal.sym(Nat, Nat.mul(one, Nat.div(d, 2n)), Nat.mul(Nat.div(d, 2n), one), NA.mul_comm(one, Nat.div(d, 2n))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.add(_, Nat.mul(one, Nat.add(Nat.div(d, 2n), Nat.mod(d, 2n))))) : Nat}
105	      %Equal.sym(Nat, Nat.mul(one, Nat.add(Nat.div(d, 2n), Nat.mod(d, 2n))), Nat.add(Nat.mul(one, Nat.div(d, 2n)), Nat.mul(one, Nat.mod(d, 2n))), NA.mul_add_left(one, Nat.div(d, 2n), Nat.mod(d, 2n))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.add(Nat.mul(Nat.div(d, 2n), one), _)) : Nat}
106	      %Equal.sym(Nat, Nat.mul(one, Nat.div(d, 2n)), Nat.mul(Nat.div(d, 2n), one), NA.mul_comm(one, Nat.div(d, 2n))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(_, Nat.mul(one, Nat.mod(d, 2n))))) : Nat}
107	      %Equal.sym(Nat, Nat.mul(one, Nat.mod(d, 2n)), Nat.mul(Nat.mod(d, 2n), one), NA.mul_comm(one, Nat.mod(d, 2n))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), _))) : Nat}
108	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(j, e), C.shift(j, e)), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one)))), Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))), NA.add_assoc(C.shift(j, e), C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) : {Nat.add(C.shift(j, e), Nat.add(C.shift(j, e), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.add(Nat.mul(Nat.div(d, 2n), one), Nat.mul(Nat.mod(d, 2n), one))))) == _ : Nat}
109	      {==}
110	
111	# the bits of n limbs below 2^16 spell their value
112	def bits_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +e: Nat, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {hv(L.bits(xs), one, e) == Nat.add(LV.pos(n, e), FS.digits(one, xs)) : Nat}:
113	  match n xs:
114	    case 0n Nil{}:
115	      %Equal.sym(Nat, Nat.add(e, 0n), e, NA.add_zero(e)) : {e == _ : Nat}
116	      {==}
117	    case 0n x <> t:
118	      Empty.absurd({hv(L.bits(x <> t), one, e) == Nat.add(LV.pos(0n, e), FS.digits(one, x <> t)) : Nat}, Lg.false_true(hx))
119	    case 1n+k Nil{}:
120	      Empty.absurd({hv(L.bits([]), one, e) == Nat.add(LV.pos(1n+k, e), FS.digits(one, [])) : Nat}, Lg.false_true(hx))
121	    case 1n+ +k +x <> +t:
122	      +hx0 = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), hx)
123	      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), hx)
124	      %Equal.sym(Nat, hv(List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)), one, e), hv(L.bits_of(16n, x), one, hv(L.bits(t), one, e)), hv_app(one, L.bits(t), e, L.bits_of(16n, x))) : {_ == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
125	      %Equal.sym(Nat, hv(L.bits_of(16n, x), one, hv(L.bits(t), one, e)), Nat.add(C.shift(16n, hv(L.bits(t), one, e)), Nat.mul(one, x)), bits_of_v(one, h1, 16n, x, hv(L.bits(t), one, e), hx0)) : {_ == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
126	      %Equal.sym(Nat, hv(L.bits(t), one, e), Nat.add(LV.pos(k, e), FS.digits(one, t)), bits_v(one, h1, k, t, e, ht)) : {Nat.add(C.shift(16n, _), Nat.mul(one, x)) == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
127	      %Equal.sym(Nat, Nat.add(LV.pos(k, e), FS.digits(one, t)), Nat.add(FS.digits(one, t), LV.pos(k, e)), NA.add_comm(LV.pos(k, e), FS.digits(one, t))) : {Nat.add(C.shift(16n, _), Nat.mul(one, x)) == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
128	      %Equal.sym(Nat, C.shift(16n, Nat.add(FS.digits(one, t), LV.pos(k, e))), Nat.add(C.shift(16n, FS.digits(one, t)), C.shift(16n, LV.pos(k, e))), WW.shift_add(16n, FS.digits(one, t), LV.pos(k, e))) : {Nat.add(_, Nat.mul(one, x)) == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
129	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, FS.digits(one, t)), C.shift(16n, LV.pos(k, e))), Nat.mul(one, x)), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))), NA.add_assoc(C.shift(16n, FS.digits(one, t)), C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))) : {_ == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
130	      %Equal.sym(Nat, Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t))), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.mul(one, x)), NA.add_comm(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : {Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))) == Nat.add(C.shift(16n, LV.pos(k, e)), _) : Nat}
131	      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.mul(one, x))), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))), NA.add_swap(C.shift(16n, LV.pos(k, e)), C.shift(16n, FS.digits(one, t)), Nat.mul(one, x))) : {Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))) == _ : Nat}
132	      {==}
133	
134	# ---- flipped bits ----
135	
136	def cbit(b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {Nat.add(Nat.sub(1n, b), b) == 1n : Nat}:
137	  match b:
138	    case 0n:
139	      {==}
140	    case 1n:
141	      {==}
142	    case 2n+ +k:
143	      Empty.absurd({Nat.add(Nat.sub(1n, 2n+k), 2n+k) == 1n : Nat}, N.lt_zero_absurd(k, hb))
144	
145	# (1 - b) one + b one = one
146	def cbit_one(+one: Nat, +b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)) == one : Nat}:
147	  %Equal.sym(Nat, Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)), Nat.mul(Nat.add(Nat.sub(1n, b), b), one), Equal.sym(Nat, Nat.mul(Nat.add(Nat.sub(1n, b), b), one), Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)), NA.mul_add_right(Nat.sub(1n, b), b, one))) : {_ == one : Nat}
148	  %Equal.sym(Nat, Nat.add(Nat.sub(1n, b), b), 1n, cbit(b, hb)) : {Nat.mul(_, one) == one : Nat}
149	  SR.one_mul(one)
150	
151	# hv(e1, flipped bits) + hv(e2, bits) + one = 2^length (e1 + e2 + one)
152	def arr(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: Nat) -> {Nat.add(Nat.add(Nat.add(a, b), Nat.add(c, d)), e) == Nat.add(Nat.add(Nat.add(a, c), e), Nat.add(b, d)) : Nat}:
153	  %Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), NA.add_assoc(a, b, Nat.add(c, d))) : {Nat.add(_, e) == Nat.add(Nat.add(Nat.add(a, c), e), Nat.add(b, d)) : Nat}
154	  %Equal.sym(Nat, Nat.add(Nat.add(a, Nat.add(b, Nat.add(c, d))), e), Nat.add(a, Nat.add(Nat.add(b, Nat.add(c, d)), e)), NA.add_assoc(a, Nat.add(b, Nat.add(c, d)), e)) : {_ == Nat.add(Nat.add(Nat.add(a, c), e), Nat.add(b, d)) : Nat}
155	  %Equal.sym(Nat, Nat.add(Nat.add(b, Nat.add(c, d)), e), Nat.add(b, Nat.add(Nat.add(c, d), e)), NA.add_assoc(b, Nat.add(c, d), e)) : {Nat.add(a, _) == Nat.add(Nat.add(Nat.add(a, c), e), Nat.add(b, d)) : Nat}
156	  %Equal.sym(Nat, Nat.add(Nat.add(c, d), e), Nat.add(c, Nat.add(d, e)), NA.add_assoc(c, d, e)) : {Nat.add(a, Nat.add(b, _)) == Nat.add(Nat.add(Nat.add(a, c), e), Nat.add(b, d)) : Nat}
157	  %Equal.sym(Nat, Nat.add(Nat.add(a, c), e), Nat.add(a, Nat.add(c, e)), NA.add_assoc(a, c, e)) : {Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, e)))) == Nat.add(_, Nat.add(b, d)) : Nat}
158	  %Equal.sym(Nat, Nat.add(Nat.add(a, Nat.add(c, e)), Nat.add(b, d)), Nat.add(a, Nat.add(Nat.add(c, e), Nat.add(b, d))), NA.add_assoc(a, Nat.add(c, e), Nat.add(b, d))) : {Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, e)))) == _ : Nat}
159	  %Equal.sym(Nat, Nat.add(Nat.add(c, e), Nat.add(b, d)), Nat.add(c, Nat.add(e, Nat.add(b, d))), NA.add_assoc(c, e, Nat.add(b, d))) : {Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, e)))) == Nat.add(a, _) : Nat}
160	  %Equal.sym(Nat, Nat.add(e, Nat.add(b, d)), Nat.add(b, Nat.add(e, d)), NA.add_swap(e, b, d)) : {Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, e)))) == Nat.add(a, Nat.add(c, _)) : Nat}
161	  %Equal.sym(Nat, Nat.add(e, d), Nat.add(d, e), NA.add_comm(e, d)) : {Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, e)))) == Nat.add(a, Nat.add(c, Nat.add(b, _))) : Nat}
162	  %Equal.sym(Nat, Nat.add(c, Nat.add(b, Nat.add(d, e))), Nat.add(b, Nat.add(c, Nat.add(d, e))), NA.add_swap(c, b, Nat.add(d, e))) : {Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, e)))) == Nat.add(a, _) : Nat}
163	  {==}
164	
165	def cb(+one: Nat, bs: List<&2, Nat>, +e1: Nat, +e2: Nat, +hb: {all01(bs) == True{} : Bool}) -> {Nat.add(Nat.add(hv(L.cbits(bs), one, e1), hv(bs, one, e2)), one) == C.shift(List.length(&2, Nat, bs), Nat.add(Nat.add(e1, e2), one)) : Nat}:
166	  match bs:
167	    case Nil{}:
168	      {==}
169	    case +b <> +t:
170	      +h0 = Lg.and_left(Nat.is_lt(b, 2n), all01(t), hb)
171	      +ht = Lg.and_right(Nat.is_lt(b, 2n), all01(t), hb)
172	      %Equal.sym(Nat, Nat.add(Nat.add(hv(L.cbits(t), one, Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.double(e1))), hv(t, one, Nat.add(Nat.mul(b, one), Nat.double(e2)))), one), C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.double(e1)), Nat.add(Nat.mul(b, one), Nat.double(e2))), one)), cb(one, t, Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.double(e1)), Nat.add(Nat.mul(b, one), Nat.double(e2)), ht)) : {_ == Nat.double(C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(e1, e2), one))) : Nat}
173	      %Equal.sym(Nat, Nat.double(C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(e1, e2), one))), C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))), Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))), Nat.double(C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(e1, e2), one))), WW.shift_dbl(List.length(&2, Nat, t), Nat.add(Nat.add(e1, e2), one)))) : {C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.double(e1)), Nat.add(Nat.mul(b, one), Nat.double(e2))), one)) == _ : Nat}
174	      %Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.double(e1)), Nat.add(Nat.mul(b, one), Nat.double(e2))), one), Nat.add(Nat.add(Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)), one), Nat.add(Nat.double(e1), Nat.double(e2))), arr(Nat.mul(Nat.sub(1n, b), one), Nat.double(e1), Nat.mul(b, one), Nat.double(e2), one)) : {C.shift(List.length(&2, Nat, t), _) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
175	      %Equal.sym(Nat, Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)), one, cbit_one(one, b, h0)) : {C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(_, one), Nat.add(Nat.double(e1), Nat.double(e2)))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
176	      %Equal.sym(Nat, Nat.double(e1), Nat.add(e1, e1), NA.double_self(e1)) : {C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(one, one), Nat.add(_, Nat.double(e2)))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
177	      %Equal.sym(Nat, Nat.double(e2), Nat.add(e2, e2), NA.double_self(e2)) : {C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(one, one), Nat.add(Nat.add(e1, e1), _))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
178	      %Equal.sym(Nat, Nat.add(Nat.add(e1, e1), Nat.add(e2, e2)), Nat.add(e1, Nat.add(e1, Nat.add(e2, e2))), NA.add_assoc(e1, e1, Nat.add(e2, e2))) : {C.shift(List.length(&2, Nat, t), Nat.add(Nat.add(one, one), _)) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
179	      %Equal.sym(Nat, Nat.add(Nat.add(one, one), Nat.add(e1, Nat.add(e1, Nat.add(e2, e2)))), Nat.add(one, Nat.add(one, Nat.add(e1, Nat.add(e1, Nat.add(e2, e2))))), NA.add_assoc(one, one, Nat.add(e1, Nat.add(e1, Nat.add(e2, e2))))) : {C.shift(List.length(&2, Nat, t), _) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
180	      %Equal.sym(Nat, Nat.add(one, Nat.add(e1, Nat.add(e1, Nat.add(e2, e2)))), Nat.add(e1, Nat.add(one, Nat.add(e1, Nat.add(e2, e2)))), NA.add_swap(one, e1, Nat.add(e1, Nat.add(e2, e2)))) : {C.shift(List.length(&2, Nat, t), Nat.add(one, _)) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
181	      %Equal.sym(Nat, Nat.add(one, Nat.add(e1, Nat.add(e2, e2))), Nat.add(e1, Nat.add(one, Nat.add(e2, e2))), NA.add_swap(one, e1, Nat.add(e2, e2))) : {C.shift(List.length(&2, Nat, t), Nat.add(one, Nat.add(e1, _))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
182	      %Equal.sym(Nat, Nat.add(one, Nat.add(e2, e2)), Nat.add(e2, Nat.add(one, e2)), NA.add_swap(one, e2, e2)) : {C.shift(List.length(&2, Nat, t), Nat.add(one, Nat.add(e1, Nat.add(e1, _)))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
183	      %Equal.sym(Nat, Nat.add(one, e2), Nat.add(e2, one), NA.add_comm(one, e2)) : {C.shift(List.length(&2, Nat, t), Nat.add(one, Nat.add(e1, Nat.add(e1, Nat.add(e2, _))))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
184	      %Equal.sym(Nat, Nat.add(one, Nat.add(e1, Nat.add(e1, Nat.add(e2, Nat.add(e2, one))))), Nat.add(e1, Nat.add(one, Nat.add(e1, Nat.add(e2, Nat.add(e2, one))))), NA.add_swap(one, e1, Nat.add(e1, Nat.add(e2, Nat.add(e2, one))))) : {C.shift(List.length(&2, Nat, t), _) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
185	      %Equal.sym(Nat, Nat.add(one, Nat.add(e1, Nat.add(e2, Nat.add(e2, one)))), Nat.add(e1, Nat.add(one, Nat.add(e2, Nat.add(e2, one)))), NA.add_swap(one, e1, Nat.add(e2, Nat.add(e2, one)))) : {C.shift(List.length(&2, Nat, t), Nat.add(e1, _)) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
186	      %Equal.sym(Nat, Nat.add(one, Nat.add(e2, Nat.add(e2, one))), Nat.add(e2, Nat.add(one, Nat.add(e2, one))), NA.add_swap(one, e2, Nat.add(e2, one))) : {C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e1, _))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
187	      %Equal.sym(Nat, Nat.add(one, Nat.add(e2, one)), Nat.add(e2, Nat.add(one, one)), NA.add_swap(one, e2, one)) : {C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e1, Nat.add(e2, _)))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
188	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))))), Nat.add(C.shift(List.length(&2, Nat, t), e1), C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))))), WW.shift_add(List.length(&2, Nat, t), e1, Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))))) : {_ == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
189	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one))))), Nat.add(C.shift(List.length(&2, Nat, t), e1), C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(e2, Nat.add(one, one))))), WW.shift_add(List.length(&2, Nat, t), e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one))))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), _) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
190	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(e2, Nat.add(one, one)))), Nat.add(C.shift(List.length(&2, Nat, t), e2), C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(one, one)))), WW.shift_add(List.length(&2, Nat, t), e2, Nat.add(e2, Nat.add(one, one)))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), _)) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
191	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(one, one))), Nat.add(C.shift(List.length(&2, Nat, t), e2), C.shift(List.length(&2, Nat, t), Nat.add(one, one))), WW.shift_add(List.length(&2, Nat, t), e2, Nat.add(one, one))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), _))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
192	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(one, one)), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)), WW.shift_add(List.length(&2, Nat, t), one, one)) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), _)))) == C.shift(List.length(&2, Nat, t), Nat.double(Nat.add(Nat.add(e1, e2), one))) : Nat}
193	      %Equal.sym(Nat, Nat.add(Nat.add(e1, e2), one), Nat.add(e1, Nat.add(e2, one)), NA.add_assoc(e1, e2, one)) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), Nat.double(_)) : Nat}
194	      %Equal.sym(Nat, Nat.double(Nat.add(e1, Nat.add(e2, one))), Nat.add(Nat.add(e1, Nat.add(e2, one)), Nat.add(e1, Nat.add(e2, one))), NA.double_self(Nat.add(e1, Nat.add(e2, one)))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), _) : Nat}
195	      %Equal.sym(Nat, Nat.add(Nat.add(e1, Nat.add(e2, one)), Nat.add(e1, Nat.add(e2, one))), Nat.add(e1, Nat.add(Nat.add(e2, one), Nat.add(e1, Nat.add(e2, one)))), NA.add_assoc(e1, Nat.add(e2, one), Nat.add(e1, Nat.add(e2, one)))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), _) : Nat}
196	      %Equal.sym(Nat, Nat.add(Nat.add(e2, one), Nat.add(e1, Nat.add(e2, one))), Nat.add(e2, Nat.add(one, Nat.add(e1, Nat.add(e2, one)))), NA.add_assoc(e2, one, Nat.add(e1, Nat.add(e2, one)))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), Nat.add(e1, _)) : Nat}
197	      %Equal.sym(Nat, Nat.add(one, Nat.add(e1, Nat.add(e2, one))), Nat.add(e1, Nat.add(one, Nat.add(e2, one))), NA.add_swap(one, e1, Nat.add(e2, one))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e2, _))) : Nat}
198	      %Equal.sym(Nat, Nat.add(one, Nat.add(e2, one)), Nat.add(e2, Nat.add(one, one)), NA.add_swap(one, e2, one)) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e2, Nat.add(e1, _)))) : Nat}
199	      %Equal.sym(Nat, Nat.add(e2, Nat.add(e1, Nat.add(e2, Nat.add(one, one)))), Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))), NA.add_swap(e2, e1, Nat.add(e2, Nat.add(one, one)))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == C.shift(List.length(&2, Nat, t), Nat.add(e1, _)) : Nat}
200	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))))), Nat.add(C.shift(List.length(&2, Nat, t), e1), C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))))), WW.shift_add(List.length(&2, Nat, t), e1, Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one)))))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == _ : Nat}
201	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one))))), Nat.add(C.shift(List.length(&2, Nat, t), e1), C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(e2, Nat.add(one, one))))), WW.shift_add(List.length(&2, Nat, t), e1, Nat.add(e2, Nat.add(e2, Nat.add(one, one))))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == Nat.add(C.shift(List.length(&2, Nat, t), e1), _) : Nat}
202	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(e2, Nat.add(one, one)))), Nat.add(C.shift(List.length(&2, Nat, t), e2), C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(one, one)))), WW.shift_add(List.length(&2, Nat, t), e2, Nat.add(e2, Nat.add(one, one)))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), _)) : Nat}
203	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(e2, Nat.add(one, one))), Nat.add(C.shift(List.length(&2, Nat, t), e2), C.shift(List.length(&2, Nat, t), Nat.add(one, one))), WW.shift_add(List.length(&2, Nat, t), e2, Nat.add(one, one))) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), _))) : Nat}
204	      %Equal.sym(Nat, C.shift(List.length(&2, Nat, t), Nat.add(one, one)), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)), WW.shift_add(List.length(&2, Nat, t), one, one)) : {Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), one), C.shift(List.length(&2, Nat, t), one)))))) == Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e1), Nat.add(C.shift(List.length(&2, Nat, t), e2), Nat.add(C.shift(List.length(&2, Nat, t), e2), _)))) : Nat}
205	      {==}
206	
207	# (a + b) + (c + d) + e = (a + c + e) + (b + d)
208	
209	def sub1_lt(b: Nat) -> {Nat.is_lt(Nat.sub(1n, b), 2n) == True{} : Bool}:
210	  match b:
211	    case 0n:
212	      {==}
213	    case 1n+k:
214	      %Equal.sym(Nat, Nat.sub(0n, k), 0n, NR.zsub(k)) : {Nat.is_lt(_, 2n) == True{} : Bool}
215	      {==}
216	
217	def cbits01(bs: List<&2, Nat>) -> {all01(L.cbits(bs)) == True{} : Bool}:
218	  match bs:
219	    case Nil{}:
220	      {==}
221	    case +b <> +t:
222	      Lg.and_intro(Nat.is_lt(Nat.sub(1n, b), 2n), all01(L.cbits(t)), sub1_lt(b), cbits01(t))