有界最小化
$ g(x, z)
を次のように定義すること
$ f(x, y)
は
原始帰納的関数
$ g(x, z)
は次のような
関数
$ z < y
かつ
$ f(x, y) = 0
となるような
$ y
が存在する時，それを満たす
$ y
の最小値を返す
$ y
が存在しない時，
$ 0
を返す(本当は
自然数
なら何でもいい)
$ g(x, z)
は
原始帰納的関数
$ g(x, z) = \mu y.(z < y \land f(x, y) = 0)
$ \mu x.M
は，
$ M
を満たす
$ x
の最小値を返すということ