def adc_t.con

lawful-words@0.1.0.0 · proof_word.bend:455

import Base

455# Subtraction is addition of the complement with carry in.
456def adc_t.con(-p: Nat, at: Word(p), bt: Word(p), sk: Bool & Bool,
457  ih: @k: Bool -> {Word.adc(p, at, bt, True{}, k) == Word.adc(p, at, Word.not(p, bt), False{}, k) : Word(p)}) ->
458  {Word.adc.con(p, at, bt, True{}, sk) == Word.adc.con(p, at, Word.not(p, bt), False{}, sk) : Word(1n+p)}:
459  match sk:
460    case (s, k):
461      %ih(k) : {WCon{s, Word.adc(p, at, bt, True{}, k)} == WCon{s, _} : Word(1n+p)}
462      {==}