let
, where
is some polynomial with integer coefficients and where
denotes "the least
such that
".
if
is a partial computable function, and
then
is a partial computable function.
let
be a PRC class, if
belongs to
, then so do the functions
and
the sum of functions can be used to construct the
quantifier in primitive recursive predicates, give a predicate
in some PRC class, it follows form the theorem that
is in PRC aswell because it simply can be represented by the function eq-unbounded-search-op-sum. the same goes for the predicate
which can be represented by the function eq-unbounded-search-op-prod.
let
belong to some given PRC class
. then by the-iter-ops the function
also belongs to
.
(taken from Martin Davis, Ron Sigal, Elaine J. Weyuker, 1994 chapter 3.7 minimalization)
if
belongs to some PRC class
and
, then
also belongs to
.
the operation
is called bounded minimalization.