Interactive tool
Formal induction sketch
Toggle base and inductive step — verdict PROVED only when both hold; otherwise NOT_PROVED. Induction ladder shows P(0) and P(k)→P(k+1). Starter: both true → PROVED.
Toggle base and inductive step — verdict PROVED only when both hold; otherwise NOT_PROVED. Induction ladder shows P(0) and P(k)→P(k+1). Starter: both true → PROVED.