proofs/crypto/secp256k1/bitsv.bend source
proofs/crypto/secp256k1/bitsv.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bitsv.src; edit the .srcimport Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../src/crypto/secp256k1/limbs.bend as Limport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Lgimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../../math/natural/arith.bend as NRimport ../../math/typed/width.bend as WWimport ./semiring.bend as SRimport ./limbs.bend as LVimport ./ineq.bend as Iimport ./reduce.bend as R# The bits of limb lists (src/crypto/secp256k1/limbs.bend bits, bits_of,# cbits) and the number they spell, most significant first, with every# bit worth `one` (hv), so that a 256-bit exponent stays symbolic.def hv(bs: List<&2, Nat>, +one: Nat, +e: Nat) -> Nat: match bs: case Nil{}: e case b <> t: hv(t, one, Nat.add(Nat.mul(b, one), Nat.double(e)))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}: match xs: case Nil{}: {==} case +x <> +t: hv_app(one, t, Nat.add(Nat.mul(x, one), Nat.double(e)), ys)def all01(bs: List<&2, Nat>) -> Bool: match bs: case Nil{}: True{} case b <> t: Bool.and(Nat.is_lt(b, 2n), all01(t))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}: match xs: case Nil{}: hy case +x <> +t: 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))def mod2_lt(+x: Nat) -> {Nat.is_lt(Nat.mod(x, 2n), 2n) == True{} : Bool}: NR.dm_lt(1n, x)def bits_of01(k: Nat, +x: Nat) -> {all01(L.bits_of(k, x)) == True{} : Bool}: match k: case 0n: {==} case 1n+ +j: 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), {==}))def bits01(xs: List<&2, Nat>) -> {all01(L.bits(xs)) == True{} : Bool}: match xs: case Nil{}: {==} case +x <> +t: all01_app(L.bits(t), L.bits_of(16n, x), bits01(t), bits_of01(16n, x))# ---- the value of bits_of ----# d < 2 s gives d / 2 < sdef two_x(+x: Nat) -> {Nat.mul(x, 2n) == Nat.add(x, x) : Nat}: %Equal.sym(Nat, Nat.mul(x, 2n), Nat.mul(2n, x), NA.mul_comm(x, 2n)) : {_ == Nat.add(x, x) : Nat} %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {Nat.add(x, _) == Nat.add(x, x) : Nat} {==}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}: +q = Nat.div(d, 2n) +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))) +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))) 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), {==})# the k bits of d < 2^k spell ddef 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}: match k: case 0n: +d0 = N.lt_succ_le(d, 0n, I.lt_subst_r(d, one, 1n, h1, hd)) +ez = N.le_antisym(d, 0n, d0, N.zero_le(d)) %Equal.sym(Nat, d, 0n, ez) : {e == Nat.add(e, Nat.mul(one, _)) : Nat} %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {e == Nat.add(e, _) : Nat} %Equal.sym(Nat, Nat.add(e, 0n), e, NA.add_zero(e)) : {e == _ : Nat} {==} case 1n+ +j: +q = Nat.div(d, 2n) +r = Nat.mod(d, 2n) %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} {==}# the bits of n limbs below 2^16 spell their valuedef 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}: match n xs: case 0n Nil{}: %Equal.sym(Nat, Nat.add(e, 0n), e, NA.add_zero(e)) : {e == _ : Nat} {==} case 0n x <> t: 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)) case 1n+k Nil{}: Empty.absurd({hv(L.bits([]), one, e) == Nat.add(LV.pos(1n+k, e), FS.digits(one, [])) : Nat}, Lg.false_true(hx)) case 1n+ +k +x <> +t: +hx0 = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), hx) +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), hx) %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} %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} %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} %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} %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} %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} %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} %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} {==}# ---- flipped bits ----def cbit(b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {Nat.add(Nat.sub(1n, b), b) == 1n : Nat}: match b: case 0n: {==} case 1n: {==} case 2n+ +k: Empty.absurd({Nat.add(Nat.sub(1n, 2n+k), 2n+k) == 1n : Nat}, N.lt_zero_absurd(k, hb))# (1 - b) one + b one = onedef 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}: %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} %Equal.sym(Nat, Nat.add(Nat.sub(1n, b), b), 1n, cbit(b, hb)) : {Nat.mul(_, one) == one : Nat} SR.one_mul(one)# hv(e1, flipped bits) + hv(e2, bits) + one = 2^length (e1 + e2 + one)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}: %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} {==}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}: match bs: case Nil{}: {==} case +b <> +t: +h0 = Lg.and_left(Nat.is_lt(b, 2n), all01(t), hb) +ht = Lg.and_right(Nat.is_lt(b, 2n), all01(t), hb) %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} {==}# (a + b) + (c + d) + e = (a + c + e) + (b + d)def sub1_lt(b: Nat) -> {Nat.is_lt(Nat.sub(1n, b), 2n) == True{} : Bool}: match b: case 0n: {==} case 1n+k: %Equal.sym(Nat, Nat.sub(0n, k), 0n, NR.zsub(k)) : {Nat.is_lt(_, 2n) == True{} : Bool} {==}def cbits01(bs: List<&2, Nat>) -> {all01(L.cbits(bs)) == True{} : Bool}: match bs: case Nil{}: {==} case +b <> +t: Lg.and_intro(Nat.is_lt(Nat.sub(1n, b), 2n), all01(L.cbits(t)), sub1_lt(b), cbits01(t))