ProofTab.gt.add_one: def of bend-osdev-gf@0.1.2.0
Import: import bend-osdev-gf@0.1.2.0/proof_tab.bend as ProofTab
Lines 108-111 of bend-osdev-gf@0.1.2.0/proof_tab.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.2.0/proof_tab.bend&start_line=108&end_line=111

import Base

# the fills' counter: i + 1 is the increment
def gt.add_one(+x: U32) -> {U32.add(x, 1) == U32.inc(x) : U32}:
  %gt.add_zero(x) : {U32.add(x, 1) == U32.inc(_) : U32}
  gt.add_inc(x, 0)

Uses (5):
  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=bend-osdev-gf@0.1.2.0/proof_tab.bend&name=gt.add_inc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.2.0/proof_tab.bend&name=gt.add_zero