def adc_not

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32alg.bend:159

import Base

159# Subtraction is addition of the complement with an incoming carry.
160def 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)}:
161  match n:
162    case 0n:
163      {==}
164    case 1n+p:
165      match a b:
166        case WCon{x, at} WCon{y, bt}:
167          adc_con_not(p, at, bt, Bool.full_add(x, Bool.not(y), c), k => adc_not(p, at, bt, k))