Every primitive recursive function is total (source code)

= Every primitive recursive function is total

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.