def un.adc_not

bend-osdev-u32@0.1.0.0 · PROOF.bend:584

import Base

584def un.adc_not(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}:
585  match n:
586    case 0n:
587      match a b:
588        case WNil{} WNil{}:
589          {==}
590    case 1n+ +p:
591      match a b c:
592        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
593          un.wcon_cong(p, True{}, Word.adc(p, at, bt, True{}, False{}), Word.adc(p, at, Word.not(p, bt), False{}, False{}), un.adc_not(p, at, bt, False{}))
594        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
595          un.wcon_cong(p, False{}, Word.adc(p, at, bt, True{}, True{}), Word.adc(p, at, Word.not(p, bt), False{}, True{}), un.adc_not(p, at, bt, True{}))
596        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
597          un.wcon_cong(p, False{}, Word.adc(p, at, bt, True{}, False{}), Word.adc(p, at, Word.not(p, bt), False{}, False{}), un.adc_not(p, at, bt, False{}))
598        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
599          un.wcon_cong(p, True{}, Word.adc(p, at, bt, True{}, False{}), Word.adc(p, at, Word.not(p, bt), False{}, False{}), un.adc_not(p, at, bt, False{}))
600        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
601          un.wcon_cong(p, False{}, Word.adc(p, at, bt, True{}, True{}), Word.adc(p, at, Word.not(p, bt), False{}, True{}), un.adc_not(p, at, bt, True{}))
602        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
603          un.wcon_cong(p, True{}, Word.adc(p, at, bt, True{}, True{}), Word.adc(p, at, Word.not(p, bt), False{}, True{}), un.adc_not(p, at, bt, True{}))
604        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
605          un.wcon_cong(p, True{}, Word.adc(p, at, bt, True{}, False{}), Word.adc(p, at, Word.not(p, bt), False{}, False{}), un.adc_not(p, at, bt, False{}))
606        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
607          un.wcon_cong(p, False{}, Word.adc(p, at, bt, True{}, True{}), Word.adc(p, at, Word.not(p, bt), False{}, True{}), un.adc_not(p, at, bt, True{}))