def ones_low

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

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/proofs/math/typed/width.bend as WW

41# only the a low bits count
42def ones_low(+a: Nat, +n: Nat) -> {SN.ones(a, C.low(a, n)) == SN.ones(a, n) : Nat}:
43  match a:
44    case 0n:
45      {==}
46    case 1n+ +p:
47      +y = C.low(p, C.half(n))
48      +eb = Equal.trans(Nat, C.bit(Nat.add(C.bit(n), Nat.double(y))), C.bit(C.bit(n)), C.bit(n), WW.bit_dbl(C.bit(n), y), bit_bit(n))
49      +eh = Equal.trans(Nat, C.half(Nat.add(C.bit(n), Nat.double(y))), Nat.add(C.half(C.bit(n)), y), y, WW.half_dbl(C.bit(n), y), Equal.cong(Nat, Nat, t => Nat.add(t, y), C.half(C.bit(n)), 0n, half_bit(n)))
50      %Equal.sym(Nat, C.bit(Nat.add(C.bit(n), Nat.double(y))), C.bit(n), eb) : {Nat.add(_, SN.ones(p, C.half(Nat.add(C.bit(n), Nat.double(y))))) == Nat.add(C.bit(n), SN.ones(p, C.half(n))) : Nat}
51      %Equal.sym(Nat, C.half(Nat.add(C.bit(n), Nat.double(y))), y, eh) : {Nat.add(C.bit(n), SN.ones(p, _)) == Nat.add(C.bit(n), SN.ones(p, C.half(n))) : Nat}
52      Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), t), SN.ones(p, y), SN.ones(p, C.half(n)), ones_low(p, C.half(n)))