Stone: Section 6

From CSWiki

Theorem 6.1: bounded for-all is primitive recursive

 We are testing whether some property is true for all numbers up to and including some number t0, the last input.
 This function has a valence of at least one, which will be used as t0. 
 Bounded for-all is always used in conjunction with some other function, p, which will serve as the test for every number 
 Syntax: [] : n is the valence minus one (as this function requires at least one input); 
 p is the function that will serve as the property which we test on all natural numbers less than t0

Theorem 6.2: bounded summation is primitive recursive

Theorem 6.3: bounded minimization is primitive recursive