PROOF.un.sub_v: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 681-692 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=681&end_line=692

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 Laws

# s + B = A + 2^n * C, from adc(a, not b, True) + 2^n * carry = 1 + A + not B
# and 1 + not B + B = 2^n
def un.sub_v(c: Bool, +n: Nat, +s: Nat, +a: Nat, +b: Nat, +nb: Nat, e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(c))) == 1n+Nat.add(a, nb) : Nat}, en: {1n+Nat.add(nb, b) == U.U32Nat.dbl(n, 1n) : Nat}) -> {Nat.add(s, b) == Nat.add(a, U.U32Nat.dbl(n, U.U32Nat.bit(Bool.not(c)))) : Nat}:
  match c:
    case True{}:
      +k = U.U32Nat.dbl(n, 1n)
      +e2 = Equal.trans(Nat, Nat.add(Nat.add(s, b), k), Nat.add(Nat.add(s, k), b), Nat.add(a, k), un.add_swap(s, b, k), Equal.trans(Nat, Nat.add(Nat.add(s, k), b), Nat.add(1n+Nat.add(a, nb), b), Nat.add(a, k), Equal.cong(Nat, Nat, v => Nat.add(v, b), Nat.add(s, k), 1n+Nat.add(a, nb), e), un.sub_mid(a, nb, b, k, en)))
      +e3 = un.add_cancel_r(Nat.add(s, b), a, k, e2)
      Equal.trans(Nat, Nat.add(s, b), a, Nat.add(a, U.U32Nat.dbl(n, 0n)), e3, Equal.trans(Nat, a, Nat.add(a, 0n), Nat.add(a, U.U32Nat.dbl(n, 0n)), Equal.sym(Nat, Nat.add(a, 0n), a, un.add_zero(a)), Equal.cong(Nat, Nat, v => Nat.add(a, v), 0n, U.U32Nat.dbl(n, 0n), Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, Laws.dbl_zero(n)))))
    case False{}:
      +e0 = Equal.trans(Nat, s, Nat.add(s, 0n), 1n+Nat.add(a, nb), Equal.sym(Nat, Nat.add(s, 0n), s, un.add_zero(s)), Equal.trans(Nat, Nat.add(s, 0n), Nat.add(s, U.U32Nat.dbl(n, 0n)), 1n+Nat.add(a, nb), Equal.cong(Nat, Nat, v => Nat.add(s, v), 0n, U.U32Nat.dbl(n, 0n), Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, Laws.dbl_zero(n))), e))
      Equal.trans(Nat, Nat.add(s, b), Nat.add(1n+Nat.add(a, nb), b), Nat.add(a, U.U32Nat.dbl(n, 1n)), Equal.cong(Nat, Nat, v => Nat.add(v, b), s, 1n+Nat.add(a, nb), e0), un.sub_mid(a, nb, b, U.U32Nat.dbl(n, 1n), en))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.sub_mid
  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