Basta aggiungere il seguente assioma
a ≠ (0,0,...0)
________________________________________
a, begin while ALL=0 do δ end ⇓ a
e la seguente regola di inferenza
a = (0,0,...0) a, begin δ end ⇓ b
b, begin while ALL=0 do δ end ⇓ c
_________________________________________________________________________________________
a, begin while ALL=0 do δ end ⇓ c
Per l'altro caso, basta sostituire le condizioni su a con le loro negazioni.