def uq.add_w

bend-osdev-algo@0.1.0.0 · proof_u32.bend:410

import Base

410# c + a + b < 2^n: adc(a, b, False, c) is c + a + b
411def 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}:
412  match n:
413    case 0n:
414      match a b c:
415        case WNil{} WNil{} False{}:
416          {==}
417        case WNil{} WNil{} True{}:
418          Empty.absurd({0n == 1n : Nat}, uq.ft(h))
419    case 1n+ +p:
420      match a b c:
421        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
422          +xa = Word.to_nat(p, at)
423          +xb = Word.to_nat(p, bt)
424          +s2 = Nat.add(xa, xb)
425          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
426          +ih = uq.add_w(p, at, bt, False{}, uq.hk0(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
427          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))
428        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
429          +xa = Word.to_nat(p, at)
430          +xb = Word.to_nat(p, bt)
431          +s2 = Nat.add(xa, xb)
432          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
433          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
434          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)))
435        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
436          +xa = Word.to_nat(p, at)
437          +xb = Word.to_nat(p, bt)
438          +s2 = Nat.add(xa, xb)
439          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
440          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
441          +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)))
442          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))
443        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
444          +xa = Word.to_nat(p, at)
445          +xb = Word.to_nat(p, bt)
446          +s2 = Nat.add(xa, xb)
447          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
448          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
449          +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)))
450          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
451          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)))
452        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
453          +xa = Word.to_nat(p, at)
454          +xb = Word.to_nat(p, bt)
455          +s2 = Nat.add(xa, xb)
456          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
457          +ih = uq.add_w(p, at, bt, False{}, uq.hk1(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
458          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)))
459        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
460          +xa = Word.to_nat(p, at)
461          +xb = Word.to_nat(p, bt)
462          +s2 = Nat.add(xa, xb)
463          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
464          +ih = uq.add_w(p, at, bt, True{}, uq.hk2(s2, dd, uq.pw(p), uq.double_add(xa, xb), h))
465          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
466          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))))
467        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
468          +xa = Word.to_nat(p, at)
469          +xb = Word.to_nat(p, bt)
470          +s2 = Nat.add(xa, xb)
471          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
472          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
473          +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)))
474          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
475          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)))
476        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
477          +xa = Word.to_nat(p, at)
478          +xb = Word.to_nat(p, bt)
479          +s2 = Nat.add(xa, xb)
480          +dd = Nat.add(Nat.double(xa), Nat.double(xb))
481          +es = uq.add_succ(Nat.double(xa), Nat.double(xb))
482          +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)))
483          +r = Word.to_nat(p, Word.adc(p, at, bt, False{}, True{}))
484          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))))