def gt.adc_carry

bend-osdev-gf@0.1.1.0 · proof_tab.bend:80

import Base

80# a + b with a carry in is (a + b) + 1
81def gt.adc_carry(n: Nat, a: Word(n), b: Word(n)) -> {Word.adc(n, a, b, False{}, True{}) == Word.inc(n, Word.adc(n, a, b, False{}, False{})) : Word(n)}:
82  match n:
83    case 0n:
84      match a b:
85        case WNil{} WNil{}:
86          {==}
87    case 1n+p:
88      match a b:
89        case WCon{False{}, at} WCon{False{}, bt}:
90          {==}
91        case WCon{True{}, +at} WCon{False{}, +bt}:
92          gt.wcon2(p, False{}, False{}, Word.adc(p, at, bt, False{}, True{}), Word.inc(p, Word.adc(p, at, bt, False{}, False{})), {==}, gt.adc_carry(p, at, bt))
93        case WCon{False{}, +at} WCon{True{}, +bt}:
94          gt.wcon2(p, False{}, False{}, Word.adc(p, at, bt, False{}, True{}), Word.inc(p, Word.adc(p, at, bt, False{}, False{})), {==}, gt.adc_carry(p, at, bt))
95        case WCon{True{}, at} WCon{True{}, bt}:
96          {==}