def add_inner

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:133

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

133def add_inner(+n: Nat, +h: Nat, +t: Nat, +c0: Nat, +c1: Nat, +c2: Nat, +ah: Nat, +bh: 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(h, Nat.add(sc(n, c1), sc(n, c2))) == Nat.add(c0, Nat.add(ah, bh)) : Nat}:
134  +rhs = Nat.add(c0, Nat.add(ah, bh))
135  %Equal.sym(Nat, Nat.add(h, Nat.add(sc(n, c1), sc(n, c2))), Nat.add(sc(n, c1), Nat.add(h, sc(n, c2))), NA.add_swap(h, sc(n, c1), sc(n, c2))) : {_ == rhs : Nat}
136  %Equal.sym(Nat, Nat.add(h, sc(n, c2)), Nat.add(t, c0), f3) : {Nat.add(sc(n, c1), _) == rhs : Nat}
137  %N.add_comm(Nat.add(t, c0), sc(n, c1)) : {_ == rhs : Nat}
138  %Equal.sym(Nat, Nat.add(Nat.add(t, c0), sc(n, c1)), Nat.add(Nat.add(t, sc(n, c1)), c0), A.add_rot(t, c0, sc(n, c1))) : {_ == rhs : Nat}
139  %Equal.sym(Nat, Nat.add(t, sc(n, c1)), Nat.add(ah, bh), f2) : {Nat.add(_, c0) == rhs : Nat}
140  N.add_comm(Nat.add(ah, bh), c0)