def cons

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

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

97def cons(+n: Nat, +a: Word(n), +b: Word(n)) -> {Nat.add(uw(n, Word.add(n, a, b)), sc(n, cy(n, a, b, False{}))) == Nat.add(uw(n, a), uw(n, b)) : Nat}:
98  AD.adc_conservation(n, a, b, False{})