Every primitive recursive function is total

ID: 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.

New to topics? Read the docs here!