ProofValue.wv.tail: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
Lines 440-441 of bend-osdev-word64@0.1.1.0/proof_value.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&start_line=440&end_line=441

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

def 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}:
  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)))))))))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.swap_mid