def gt.add_one

bend-osdev-gf@0.1.1.0 · proof_tab.bend:108

import Base

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