def bc_go

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:116

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN

116def bc_go(+k: Nat, +x: U32) -> {F.u32_bc_go(k, x) == SN.ones(q4(k), U32.to_nat(x)) : Nat}:
117  match k:
118    case 0n:
119      {==}
120    case 1n+ +p:
121      +vx = U32.to_nat(x)
122      +ih = Equal.trans(Nat, F.u32_bc_go(p, U32.shrn(x, 4n)), SN.ones(q4(p), U32.to_nat(U32.shrn(x, 4n))), SN.ones(q4(p), C.high(4n, vx)), bc_go(p, U32.shrn(x, 4n)), Equal.cong(Nat, Nat, t => SN.ones(q4(p), t), U32.to_nat(U32.shrn(x, 4n)), C.high(4n, vx), SHN.shrn_high(x, 4n)))
123      +e1 = Equal.cong(Nat, Nat, t => Nat.add(t, F.u32_bc_go(p, U32.shrn(x, 4n))), F.ones4(U32.to_nat(U32.mod(x, 16))), SN.ones(4n, vx), nib_ones(x))
124      +e2 = Equal.cong(Nat, Nat, t => Nat.add(SN.ones(4n, vx), t), F.u32_bc_go(p, U32.shrn(x, 4n)), SN.ones(q4(p), C.high(4n, vx)), ih)
125      Equal.trans(Nat, Nat.add(F.ones4(U32.to_nat(U32.mod(x, 16))), F.u32_bc_go(p, U32.shrn(x, 4n))), Nat.add(SN.ones(4n, vx), F.u32_bc_go(p, U32.shrn(x, 4n))), SN.ones(Nat.add(4n, q4(p)), vx), e1, Equal.trans(Nat, Nat.add(SN.ones(4n, vx), F.u32_bc_go(p, U32.shrn(x, 4n))), Nat.add(SN.ones(4n, vx), SN.ones(q4(p), C.high(4n, vx))), SN.ones(Nat.add(4n, q4(p)), vx), e2, Equal.sym(Nat, SN.ones(Nat.add(4n, q4(p)), vx), Nat.add(SN.ones(4n, vx), SN.ones(q4(p), C.high(4n, vx))), ones_add(4n, q4(p), vx))))