def wv.nsub

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

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

447# Subtraction: the halves with their borrows put together
448def wv.nsub(+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, bl) == Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))) : Nat}, e2: {Nat.add(t, bh) == Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))) : Nat}, e3: {Nat.add(h, b1) == Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))) : Nat}, eb: {b1 == U.U32Nat.bit(cb) : Nat}) -> {Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), Nat.add(bl, U.U32Nat.dbl(n, bh))) == Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))) : Nat}:
449  +ez = Equal.trans(Nat, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)), Nat.add(Nat.add(U.U32Nat.bit(cb), h), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.bit(cb), h), bh), Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)), UL.nat_add_assoc(U.U32Nat.bit(cb), h, bh)), Equal.trans(Nat, Nat.add(Nat.add(U.U32Nat.bit(cb), h), bh), Nat.add(Nat.add(h, U.U32Nat.bit(cb)), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, bh), Nat.add(U.U32Nat.bit(cb), h), Nat.add(h, U.U32Nat.bit(cb)), UL.nat_add_comm(U.U32Nat.bit(cb), h)), Equal.trans(Nat, Nat.add(Nat.add(h, U.U32Nat.bit(cb)), bh), Nat.add(Nat.add(h, b1), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(h, v), bh), U.U32Nat.bit(cb), b1, Equal.sym(Nat, b1, U.U32Nat.bit(cb), eb)), Equal.trans(Nat, Nat.add(Nat.add(h, b1), bh), Nat.add(Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), bh), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, bh), Nat.add(h, b1), Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), e3), Equal.trans(Nat, Nat.add(Nat.add(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), bh), Nat.add(Nat.add(t, bh), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), wn.add_swap(t, U.U32Nat.dbl(n, U.U32Nat.bit(c3)), bh), Equal.trans(Nat, Nat.add(Nat.add(t, bh), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(t, bh), Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), e2), Equal.trans(Nat, Nat.add(Nat.add(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2))), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Nat.add(ah, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3)))), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), UL.nat_add_assoc(ah, U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), Equal.cong(Nat, Nat, v => Nat.add(ah, v), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(c2)), U.U32Nat.dbl(n, U.U32Nat.bit(c3))), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))), Equal.sym(Nat, 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)))))))))))
450  Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, h)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(l, bl), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), wn.swap_mid(l, U.U32Nat.dbl(n, h), bl, U.U32Nat.dbl(n, bh)), Equal.trans(Nat, Nat.add(Nat.add(l, bl), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(l, bl), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(l, bl), v), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh)), U.U32Nat.dbl(n, Nat.add(h, bh)), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(h, bh)), Nat.add(U.U32Nat.dbl(n, h), U.U32Nat.dbl(n, bh)), UL.dbl_add(n, h, bh))), Equal.trans(Nat, Nat.add(Nat.add(l, bl), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(l, bl), Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), e1), Equal.trans(Nat, Nat.add(Nat.add(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(h, bh))), Nat.add(al, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh)))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), UL.nat_add_assoc(al, U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh))), Equal.trans(Nat, Nat.add(al, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh)))), Nat.add(al, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(al, v), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh))), U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh))), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(cb)), U.U32Nat.dbl(n, Nat.add(h, bh))), UL.dbl_add(n, U.U32Nat.bit(cb), Nat.add(h, bh)))), Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)))), Nat.add(al, U.U32Nat.dbl(n, Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(al, U.U32Nat.dbl(n, v)), Nat.add(U.U32Nat.bit(cb), Nat.add(h, bh)), Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), ez), Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(al, Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), wv.Q(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))), Equal.cong(Nat, Nat, v => Nat.add(al, v), U.U32Nat.dbl(n, Nat.add(ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), UL.dbl_add(n, ah, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), Equal.sym(Nat, Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3))))), Nat.add(al, Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))), UL.nat_add_assoc(al, U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.bit(c2), U.U32Nat.bit(c3)))))))))))))