ProofU32.uq.sub_w: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
Lines 318-377 of bend-osdev-algo@0.1.0.0/proof_u32.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&start_line=318&end_line=377

import Base

# for b <= a (b < a when the carry in c is False):
# a = adc(a, b, True, c) + (1 - c) + b
def uq.sub_w(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_le(Nat.add(uq.cb(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) -> {Word.to_nat(n, a) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, True{}, c)), Nat.add(uq.cb(c), Word.to_nat(n, b))) : Nat}:
  match n:
    case 0n:
      match a b c:
        case WNil{} WNil{} True{}:
          {==}
        case WNil{} WNil{} False{}:
          Empty.absurd({0n == 1n : Nat}, uq.ft(h))
    case 1n+ +p:
      match a b c:
        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.ha(yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
          uq.double_add(r, yv)
        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
          uq.alg2(r, yv)
        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.hc(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
          uq.succ_cong(Nat.double(Nat.add(r, yv)), Nat.add(Nat.double(r), Nat.double(yv)), uq.double_add(r, yv))
        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
          uq.alg6(r, yv)
        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
          uq.alg2(r, yv)
        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.ha(1n+yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
          uq.alg4(r, yv)
        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
          %Equal.sym(Nat, xv, Nat.add(r, yv), uq.sub_w(p, at, bt, True{}, uq.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
          uq.alg6(r, yv)
        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
          +xv = Word.to_nat(p, at)
          +yv = Word.to_nat(p, bt)
          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), uq.sub_w(p, at, bt, False{}, uq.hb(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
          uq.succ_cong(Nat.double(Nat.add(r, 1n+yv)), Nat.add(Nat.double(r), 2n+Nat.double(yv)), uq.alg4(r, yv))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.alg2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.alg4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.alg6
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.cb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.double_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.ha
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.hb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.hc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.succ_cong