def wv.nadd

bend-osdev-word64@0.1.1.0 · proof_value.bend:443

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

443def wv.nadd(+n: Nat, +cb: Bool, +c2: Bool, +c3: Bool, +l: Nat, +t: Nat, +h: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +b1: Nat, e1: {Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))) == Nat.add(al, bl) : Nat}, e2: {Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c2))) == Nat.add(ah, bh) : Nat}, e3: {Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))) == Nat.add(t, b1) : Nat}, eb: {b1 == U.U32Nat.bit(cb) : Nat}) -> {Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))) == Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Nat}:
444  +ey = Equal.trans(Nat, Nat.add(h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Nat.add(Nat.add(ah, bh), b1), Equal.cong(Nat, Nat, v => Nat.add(h, v), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), UL.dbl_add(n, U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Equal.trans(Nat, Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), Nat.add(Nat.add(ah, bh), b1), Equal.cong(Nat, Nat, v => Nat.add(h, v), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), UL.nat_add_comm(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Equal.trans(Nat, Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), Nat.add(Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(ah, bh), b1), Equal.sym(Nat, Nat.add(Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(h, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), UL.nat_add_assoc(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3)), U.U32Nat.dbl(n, U.U32Nat.bit(c2)))), Equal.trans(Nat, Nat.add(Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(t, b1), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(ah, bh), b1), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(h, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(t, b1), e3), Equal.trans(Nat, Nat.add(Nat.add(t, b1), U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), b1), Nat.add(Nat.add(ah, bh), b1), wn.add_swap(t, b1, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Equal.cong(Nat, Nat, v => Nat.add(v, b1), Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), Nat.add(ah, bh), e2))))))
445  Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Nat.add(l, U.U32Nat.dbl(n, Nat.add(h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), wv.pre(n, l, h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), wv.tail(n, cb, l, Nat.add(h, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), al, bl, ah, bh, b1, e1, eb, ey))