A second technique is that if you're lucky the predicate that you've used to define your state space is stronger than the invariant you're trying to prove. So regardless of whether a state is reachable or not, you can prove the invariant holds:
where P is the predicate describing your set of states. If it's true of every state, then certainly it's true of every reachable state.
For example, recall in the Counter example, the predicate P is simply
. Hence we can trivially show the invariant property
holds:
