ProofU32.uq.add_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 410-484 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=410&end_line=484

import Base

# c + a + b < 2^n: adc(a, b, False, c) is c + a + b
def uq.add_w(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_lt(Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), uq.pw(n)) == True{} : Bool}) -> {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}:
  match n:
    case 0n:
      match a b c:
        case WNil{} WNil{} False{}:
          {==}
        case WNil{} WNil{} True{}:
          Empty.absurd({0n == 1n : Nat}, uq.ft(h))
    case 1n+ +p:
      match a b c:
        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, False{}, uq.hk0(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
          Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb))
        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
          uq.succ_cong(Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), dd, Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb)))
        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, Nat.double(uq.pw(p)), es, h)))
          Equal.trans(Nat, 1n+Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), 1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), uq.succ_cong(Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), dd, Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb))), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es))
        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 2n+dd, Nat.double(uq.pw(p)), uq.succ_cong(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es), h)))
          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
          Equal.trans(Nat, Nat.double(r), 2n+dd, 1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb)))), uq.succ_cong(1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es)))
        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
          uq.succ_cong(Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), dd, Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{}))), Nat.double(s2), dd, uq.double_cong(Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})), s2, ih), uq.double_add(xa, xb)))
        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
          Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb))))
        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 2n+dd, Nat.double(uq.pw(p)), uq.succ_cong(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es), h)))
          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
          Equal.trans(Nat, Nat.double(r), 2n+dd, 1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb)))), uq.succ_cong(1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es)))
        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
          +xa = Word.to_nat(p, at)
          +xb = Word.to_nat(p, bt)
          +s2 = Nat.add(xa, xb)
          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
          +ih = uq.add_w(p, at, bt, True{}, uq.hk3(s2, dd, uq.pw(p), uq.double_add(xa, xb), uq.lt_rw(2n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 3n+dd, Nat.double(uq.pw(p)), uq.succ_cong(1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 2n+dd, uq.succ_cong(Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es)), h)))
          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
          Equal.trans(Nat, 1n+Nat.double(r), 3n+dd, 2n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), uq.succ_cong(Nat.double(r), 2n+dd, Equal.trans(Nat, Nat.double(r), 2n+Nat.double(s2), 2n+dd, uq.double_cong(r, 1n+s2, ih), uq.succ_cong(1n+Nat.double(s2), 1n+dd, uq.succ_cong(Nat.double(s2), dd, uq.double_add(xa, xb))))), uq.succ_cong(2n+dd, 1n+Nat.add(Nat.double(xa), 1n+Nat.double(xb)), uq.succ_cong(1n+dd, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), Equal.sym(Nat, Nat.add(Nat.double(xa), 1n+Nat.double(xb)), 1n+dd, es))))

Uses (25):
  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=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=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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.add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.cv
  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.double_cong
  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.hk0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.hk1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.hk2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.hk3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.lt_rw
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.pw
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.succ_cong