def add_alg

bend-collections-laws-math@1.0.0.0 · proofs/lib/word.bend:142

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as PR

142# low limbs l with carry c0, high limbs t = ah + bh (carry c1), then h = t + c0
143# (carry c2): the two-limb sum loses exactly 2^(2n) (c1 + c2).
144def add_alg(+n: Nat, +l: Nat, +h: Nat, +t: Nat, +c0: Nat, +c1: Nat, +c2: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +f1: {Nat.add(l, sc(n, c0)) == Nat.add(al, bl) : Nat}, +f2: {Nat.add(t, sc(n, c1)) == Nat.add(ah, bh) : Nat}, +f3: {Nat.add(h, sc(n, c2)) == Nat.add(t, c0) : Nat}) -> {Nat.add(Nat.add(l, sc(n, h)), sc(n, sc(n, Nat.add(c1, c2)))) == Nat.add(Nat.add(al, sc(n, ah)), Nat.add(bl, sc(n, bh))) : Nat}:
145  +x = Nat.add(sc(n, c1), sc(n, c2))
146  +rhs = Nat.add(Nat.add(al, sc(n, ah)), Nat.add(bl, sc(n, bh)))
147  %A.sc_add(n, c1, c2) : {Nat.add(Nat.add(l, sc(n, h)), sc(n, _)) == rhs : Nat}
148  %Equal.sym(Nat, Nat.add(Nat.add(l, sc(n, h)), sc(n, x)), Nat.add(l, Nat.add(sc(n, h), sc(n, x))), N.add_assoc(l, sc(n, h), sc(n, x))) : {_ == rhs : Nat}
149  %Equal.sym(Nat, Nat.add(sc(n, h), sc(n, x)), sc(n, Nat.add(h, x)), A.sc_add(n, h, x)) : {Nat.add(l, _) == rhs : Nat}
150  %Equal.sym(Nat, Nat.add(h, x), Nat.add(c0, Nat.add(ah, bh)), add_inner(n, h, t, c0, c1, c2, ah, bh, f2, f3)) : {Nat.add(l, sc(n, _)) == rhs : Nat}
151  %A.sc_add(n, c0, Nat.add(ah, bh)) : {Nat.add(l, _) == rhs : Nat}
152  %N.add_assoc(l, sc(n, c0), sc(n, Nat.add(ah, bh))) : {_ == rhs : Nat}
153  %Equal.sym(Nat, Nat.add(l, sc(n, c0)), Nat.add(al, bl), f1) : {Nat.add(_, sc(n, Nat.add(ah, bh))) == rhs : Nat}
154  %A.sc_add(n, ah, bh) : {Nat.add(Nat.add(al, bl), _) == rhs : Nat}
155  PR.shuffle(al, bl, sc(n, ah), sc(n, bh))