How do we show that a predicate is an invariant? There are lots of techniques. If the state machine is finite, you can do an exhaustive case analysis and show that it holds for every state. This technique is fine if there are a small number of states or if you have a tool called a model checker handy (you will in your Analysis core course next semester).
If your state machine is infinite, you must resort to something else. I'm going to sketch out three techniques. They can all also be used if your state machine is finite. Technique C is the one most often used in practice.