Prova de Invariância

Prova-se a invariância de um predicado P de estado por indução:
- Base: provar que P é invariante para computações de tamanho 1;
- Indução: supondo que P é invariante para toda computação de tamanho n, provar que P é invariante para toda computação de tamanho n+1.
Em outras palavras:
- Base: provar P(q₀);
- Indução: para todo comando guardado $\gamma = (g,a)$ , mostrar que
  
  $\begin{displaymath} \forall q, q' \in Q, q' = a(q), P(q) \wedge g(q) \Longrightarrow P(q')\end{displaymath}$ (1)
  
  (Obs.: $\wedge$ é a notação para o ``e'' lógico, e $\vee$ para o ``ou''.)
Ou: uma computação só pode ser prolongada por um comando cuja guarda é válida, e só precisamos considerar prolongamentos de computações P-invariantes.