def wv.tail

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

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

440def wv.tail(+n: Nat, +cb: Bool, +l: Nat, +y: Nat, +al: Nat, +bl: Nat, +ah: Nat, +bh: Nat, +b1: Nat, e1: {Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))) == Nat.add(al, bl) : Nat}, eb: {b1 == U.U32Nat.bit(cb) : Nat}, ey: {y == Nat.add(Nat.add(ah, bh), b1) : Nat}) -> {Nat.add(l, U.U32Nat.dbl(n, y)) == Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Nat}:
441  Equal.trans(Nat, Nat.add(l, U.U32Nat.dbl(n, y)), Nat.add(l, U.U32Nat.dbl(n, Nat.add(Nat.add(ah, bh), b1))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(l, U.U32Nat.dbl(n, v)), y, Nat.add(Nat.add(ah, bh), b1), ey), Equal.trans(Nat, Nat.add(l, U.U32Nat.dbl(n, Nat.add(Nat.add(ah, bh), b1))), Nat.add(l, Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(l, v), U.U32Nat.dbl(n, Nat.add(Nat.add(ah, bh), b1)), Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1)), UL.dbl_add(n, Nat.add(ah, bh), b1)), Equal.trans(Nat, Nat.add(l, Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1))), Nat.add(l, Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(l, v), Nat.add(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1)), Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh))), UL.nat_add_comm(U.U32Nat.dbl(n, Nat.add(ah, bh)), U.U32Nat.dbl(n, b1))), Equal.trans(Nat, Nat.add(l, Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), Nat.add(Nat.add(l, U.U32Nat.dbl(n, b1)), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.sym(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, b1)), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(l, Nat.add(U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), UL.nat_add_assoc(l, U.U32Nat.dbl(n, b1), U.U32Nat.dbl(n, Nat.add(ah, bh)))), Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, b1)), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(l, U.U32Nat.dbl(n, v)), U.U32Nat.dbl(n, Nat.add(ah, bh))), b1, U.U32Nat.bit(cb), eb), Equal.trans(Nat, Nat.add(Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, bl), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(v, U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(l, U.U32Nat.dbl(n, U.U32Nat.bit(cb))), Nat.add(al, bl), e1), Equal.trans(Nat, Nat.add(Nat.add(al, bl), U.U32Nat.dbl(n, Nat.add(ah, bh))), Nat.add(Nat.add(al, bl), Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, bh))), Nat.add(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))), Equal.cong(Nat, Nat, v => Nat.add(Nat.add(al, bl), v), U.U32Nat.dbl(n, Nat.add(ah, bh)), Nat.add(U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, bh)), UL.dbl_add(n, ah, bh)), wn.swap_mid(al, bl, U.U32Nat.dbl(n, ah), U.U32Nat.dbl(n, bh)))))))))