GNU Aris Manual: in

---

6.5.4 Induction

• P(z(a))
• P(x) → P(s(x))
• ——–
• Vx(P(x))

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))’.