9.2 Induction

Mathematical induction requires a base case, and an inductive step. In Aris, this is used in conjunction with seqlog. For seqlog, the induction scheme is:

• Vx(P(z(x)) ^ (P(x) → P(s(x)))) → Vx(P(x))