def cons_sub

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:189

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as AD

189def cons_sub(+n: Nat, +x: Word(n), +a: Word(n)) -> {Nat.add(uw(n, Word.sub(n, x, a)), sc(n, cy(n, x, Word.not(n, a), True{}))) == Nat.add(1n, Nat.add(uw(n, x), uw(n, Word.not(n, a)))) : Nat}:
190  %Equal.sym(Word(n), Word.adc(n, x, a, True{}, True{}), Word.adc(n, x, Word.not(n, a), False{}, True{}), adc_not(n, x, a, True{})) : {Nat.add(uw(n, _), sc(n, cy(n, x, Word.not(n, a), True{}))) == Nat.add(1n, Nat.add(uw(n, x), uw(n, Word.not(n, a)))) : Nat}
191  AD.adc_conservation(n, x, Word.not(n, a), True{})