A. Use induction over states in executions.

When you have to reason about an infinite domain, the technique that should spring to mind is induction. Induction is especially appropriate when there is a natural, often recursive, structure to your domain. Since what we want to prove is that a property is true of every state of every execution of the state machine, then I can induct over the states in the sequence of states of every execution. Recall that an execution looks like:

Then to prove a property, , is invariant requires that for every execution:

1. Base Case: I show it holds in the initial state , and
2. Inductive Step: I assume it holds in state and show that it holds in state .