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.