proofs/crypto/secp256k1/bitsv.bend

bend-collections-laws-crypto@1.0.0.0 · 222 lines · 17 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bitsv.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/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
20def 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
25def 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
32def 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
37def 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
44def mod2_lt(+x: Nat) -> {Nat.is_lt(Nat.mod(x, 2n), 2n) == True{} : Bool}:
45  NR.dm_lt(1n, x)
46
47def 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
54def 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
64def 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
69def 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
76def 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
112def 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
136def 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
146def 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)
152def 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
165def 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
209def 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
217def 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))