ProofTab.gt.add_inc: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab
Lines 103-106 of bend-osdev-gf@0.1.1.0/proof_tab.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&start_line=103&end_line=106

import Base

def gt.add_inc(a: U32, b: U32) -> {U32.add(a, U32.inc(b)) == U32.inc(U32.add(a, b)) : U32}:
  match a b:
    case U32{+x} U32{+y}:
      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)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.inc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.adc_carry
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.adc_inc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.u32_cong