def ones_add

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

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/lib/nat.bend as N

54def ones_add(+a: Nat, +b: Nat, +n: Nat) -> {SN.ones(Nat.add(a, b), n) == Nat.add(SN.ones(a, n), SN.ones(b, C.high(a, n))) : Nat}:
55  match a:
56    case 0n:
57      Equal.sym(Nat, Nat.add(0n, SN.ones(b, n)), SN.ones(b, n), Equal.trans(Nat, Nat.add(0n, SN.ones(b, n)), Nat.add(SN.ones(b, n), 0n), SN.ones(b, n), N.add_comm(0n, SN.ones(b, n)), N.add_zero(SN.ones(b, n))))
58    case 1n+ +p:
59      +ih = ones_add(p, b, C.half(n))
60      Equal.trans(Nat, Nat.add(C.bit(n), SN.ones(Nat.add(p, b), C.half(n))), Nat.add(C.bit(n), Nat.add(SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n))))), Nat.add(Nat.add(C.bit(n), SN.ones(p, C.half(n))), SN.ones(b, C.high(p, C.half(n)))), Equal.cong(Nat, Nat, t => Nat.add(C.bit(n), t), SN.ones(Nat.add(p, b), C.half(n)), Nat.add(SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n)))), ih), Equal.sym(Nat, Nat.add(Nat.add(C.bit(n), SN.ones(p, C.half(n))), SN.ones(b, C.high(p, C.half(n)))), Nat.add(C.bit(n), Nat.add(SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n))))), N.add_assoc(C.bit(n), SN.ones(p, C.half(n)), SN.ones(b, C.high(p, C.half(n))))))