Previous: sq, Up: Miscellaneous Rules [Contents]

This rule is how Aris implements mathematical induction. ‘P(z(x))’ is the base case, and the inductive step is ‘P(x)’ → ‘P(s(x))’.