# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bitsv.src; edit the .src
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WW
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./ineq.bend as I
import ./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 < s
def 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 d
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}:
  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 value
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}:
  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 = one
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}:
  %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))