def AP.adc

bend-osdev-array@0.1.0.1 · PROOF.bend:257

import Base

257# for b <= a (b < a when the carry in c is False):
258# a = adc(a, b, True, c) + (1 - c) + b
259def AP.adc(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_le(Nat.add(AP.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(AP.cb(c), Word.to_nat(n, b))) : Nat}:
260  match n:
261    case 0n:
262      match a b c:
263        case WNil{} WNil{} True{}:
264          {==}
265        case WNil{} WNil{} False{}:
266          Empty.absurd({0n == 1n : Nat}, AP.ft(h))
267    case 1n+ +p:
268      match a b c:
269        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
270          +xv = Word.to_nat(p, at)
271          +yv = Word.to_nat(p, bt)
272          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
273          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
274          AP.double_add(r, yv)
275        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
276          +xv = Word.to_nat(p, at)
277          +yv = Word.to_nat(p, bt)
278          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
279          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
280          AP.alg2(r, yv)
281        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
282          +xv = Word.to_nat(p, at)
283          +yv = Word.to_nat(p, bt)
284          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
285          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.hc(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
286          AP.succ_cong(Nat.double(Nat.add(r, yv)), Nat.add(Nat.double(r), Nat.double(yv)), AP.double_add(r, yv))
287        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
288          +xv = Word.to_nat(p, at)
289          +yv = Word.to_nat(p, bt)
290          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
291          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
292          AP.alg6(r, yv)
293        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
294          +xv = Word.to_nat(p, at)
295          +yv = Word.to_nat(p, bt)
296          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
297          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
298          AP.alg2(r, yv)
299        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
300          +xv = Word.to_nat(p, at)
301          +yv = Word.to_nat(p, bt)
302          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
303          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.ha(1n+yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
304          AP.alg4(r, yv)
305        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
306          +xv = Word.to_nat(p, at)
307          +yv = Word.to_nat(p, bt)
308          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
309          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
310          AP.alg6(r, yv)
311        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
312          +xv = Word.to_nat(p, at)
313          +yv = Word.to_nat(p, bt)
314          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
315          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
316          AP.succ_cong(Nat.double(Nat.add(r, 1n+yv)), Nat.add(Nat.double(r), 2n+Nat.double(yv)), AP.alg4(r, yv))