Structural induction for primitive recursive functions

To prove a property of every primitive recursive function, prove it for the zero, successor, and projection functions, then prove that it is preserved by composition and by primitive recursion. This is structural induction on the finite construction of the function.

The initial functions are total, composition preserves totality, and ordinary induction on the recursion argument shows that primitive recursion applied to total functions is total. Structural induction therefore proves that every primitive recursive function is total.