Bounded search asks about the first N steps from reset. Induction asks about every step, by splitting the question in two: the property holds for the first k states from reset, and any k consecutive states that follow the transition relation and satisfy it are followed by a state that satisfies it. A pass needs both halves to the same k. When the second half fails from a state reset can never reach, the trace is a counterexample to induction, and the cure is a helper invariant that excludes the unreachable region. The decade counter carries the whole topic: its never-15 property is true on every reachable state, and not inductive.
Lesson | After it you can... |
|---|---|
State both obligations and refuse a base-only verdict. | |
Read a step failure and decide spurious or real. | |
Write the helper that makes a property inductive and prove the helper. | |
Mine candidate invariants from traces and check them by proof. |
Suggested order: top to bottom. The two obligations first, because everything else is commentary on the step. The step-failure reading second, because helpers are written against CTIs. Strengthening third, because it applies the reading. Discovery last, because mining only makes sense once you know what a good invariant looks like. The first-principles induction lesson is the prerequisite: this topic starts where its k equal to 1 helper leaves off.
The base covers the first k states from reset and the step covers every state after them: a shorter base leaves middle states covered by neither half. Reading the base half as a proof is the classic misread the first lesson demonstrates.