Technique A requires that we reason in terms of first principles-- using structural induction (over states in executions)--which can sometimes be cumbersome. And, usually, of course, we are not so lucky as in Technique B. Technique C is an alternative inductive proof strategy that is usually more manageable than Technique A: we do a case analysis of all actions, which indirectly proves the same thing as in Technique A.
At the bottom of p. 1
when I argued that the Counter's invariant holds,
we need to show that the invariant holds in each initial state
and then for each action
show that if the
invariant holds in its pre-state, it holds in the post-state.
In general, we have a proof rule that looks like:
where I is the set of initial states and A is the set of
actions.
and 
are the pre- and post-conditions of a, respectively.
Or, said in English:
is true for each initial state. holds in the pre-state, holds in the pre-state, and holds in the pre- and post-states, then
holds in the post-state.
is an invariant.
The two main proof steps are sometimes called (1) establishing the invariant (true in initial states) and (2) preserving the invariant (assuming it's true in a pre-state and showing that each action's the post-state preserves it).
What's the rationale for this proof rule? First, notice I care only
about reachable states (that's why the 
appears above).
Second, consider any execution of my state machine:
As in Technique A I need to make sure that holds in 
(establishing the invariant). Also,
for any pair of successive states, 
, in
the
execution, if I assume holds in 
then I need to show
it holds in 
. Since the only way I can get from any to
the next state is by one of the actions a in A, then if I
show the invariant if preserved for each a, I've shown for each
reachable state
the
invariant holds.