def gt.add_inc
bend-osdev-gf@0.1.1.0 · proof_tab.bend:103
import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab
import Base
103def gt.add_inc(a: U32, b: U32) -> {U32.add(a, U32.inc(b)) == U32.inc(U32.add(a, b)) : U32}:
104 match a b:
105 case U32{+x} U32{+y}:
106 gt.u32_cong(Word.adc(32n, x, Word.inc(32n, y), False{}, False{}), Word.inc(32n, Word.adc(32n, x, y, False{}, False{})), Equal.trans(Word(32n), Word.adc(32n, x, Word.inc(32n, y), False{}, False{}), Word.adc(32n, x, y, False{}, True{}), Word.inc(32n, Word.adc(32n, x, y, False{}, False{})), gt.adc_inc(32n, x, y), gt.adc_carry(32n, x, y)))