def uq.sub_w

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

import Base

318# for b <= a (b < a when the carry in c is False):
319# a = adc(a, b, True, c) + (1 - c) + b
320def 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}:
321  match n:
322    case 0n:
323      match a b c:
324        case WNil{} WNil{} True{}:
325          {==}
326        case WNil{} WNil{} False{}:
327          Empty.absurd({0n == 1n : Nat}, uq.ft(h))
328    case 1n+ +p:
329      match a b c:
330        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
331          +xv = Word.to_nat(p, at)
332          +yv = Word.to_nat(p, bt)
333          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
334          %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}
335          uq.double_add(r, yv)
336        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
337          +xv = Word.to_nat(p, at)
338          +yv = Word.to_nat(p, bt)
339          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
340          %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}
341          uq.alg2(r, yv)
342        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
343          +xv = Word.to_nat(p, at)
344          +yv = Word.to_nat(p, bt)
345          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
346          %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}
347          uq.succ_cong(Nat.double(Nat.add(r, yv)), Nat.add(Nat.double(r), Nat.double(yv)), uq.double_add(r, yv))
348        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
349          +xv = Word.to_nat(p, at)
350          +yv = Word.to_nat(p, bt)
351          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
352          %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}
353          uq.alg6(r, yv)
354        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
355          +xv = Word.to_nat(p, at)
356          +yv = Word.to_nat(p, bt)
357          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
358          %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}
359          uq.alg2(r, yv)
360        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
361          +xv = Word.to_nat(p, at)
362          +yv = Word.to_nat(p, bt)
363          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
364          %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}
365          uq.alg4(r, yv)
366        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
367          +xv = Word.to_nat(p, at)
368          +yv = Word.to_nat(p, bt)
369          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
370          %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}
371          uq.alg6(r, yv)
372        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
373          +xv = Word.to_nat(p, at)
374          +yv = Word.to_nat(p, bt)
375          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
376          %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}
377          uq.succ_cong(Nat.double(Nat.add(r, 1n+yv)), Nat.add(Nat.double(r), 2n+Nat.double(yv)), uq.alg4(r, yv))