Invariante correttezza parziale e totale:

$$ i \equiv v = 3^{h+1} \land h\leq M $$

Espressione $E$ per correttezza totale:

$$ E = M-h $$

1. Tutti gli stati

2. $AFv$ vale negli stati 2, 4

   → $EG(AFv)$ vale negli stati 1, 2, 4

   Nello stato 3 non esiste un cammino dove vale globalmente $AFv$