def gt.adc_zero

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

import Base

49def gt.adc_zero(n: Nat, w: Word(n)) -> {Word.adc(n, w, Word.zero(n), False{}, False{}) == w : Word(n)}:
50  match n:
51    case 0n:
52      match w:
53        case WNil{}:
54          {==}
55    case 1n+p:
56      match w:
57        case WCon{False{}, +t}:
58          gt.wcon2(p, False{}, False{}, Word.adc(p, t, Word.zero(p), False{}, False{}), t, {==}, gt.adc_zero(p, t))
59        case WCon{True{}, +t}:
60          gt.wcon2(p, True{}, True{}, Word.adc(p, t, Word.zero(p), False{}, False{}), t, {==}, gt.adc_zero(p, t))