Es sei der das Programm repräsentierende Ausdruck im Sinne von
Fakt
in den Variablen
(zur Notationsvereinfachung schreiben wir also statt und statt .).
Es sei der Ausdruck
(in den vier freien Variablen ),
der die
-Funktion
arithmetisch repräsentiert.
Der Ausdruck
-
ist also genau dann wahr in , wenn
ist. Diese Beziehung verwenden wir für
(bzw. )
und
(bzw. )
und
.
Daher ist der Ausdruck
(in den freien Variablen )
-
bei Interpretation in genau dann wahr, wenn die -Funktion für die aufeinander folgenden Zahlen
(eingesetzt in die dritte Komponente der -Funktion)
gleich und für die aufeinander folgenden Zahlen gleich ist. An der mit bezeichneten Stelle in steht die -fache Addition der Variablen mit sich selbst plus die -fache Addition der .
Mit diesem Ausdruck soll der Konfigurationsübergang beim -ten Rechenschritt beschrieben werden. Da man die Registerbelegung beim -ten Rechenschritt nicht von vornherein kennt, muss man den Übergang mit Allquantoren ansetzen. Der Ausdruck
-
besagt, dass der durch über die -Funktion kodierte Konfigurationsübergang durch das Programm bewirkt wird.
In analoger Weise ist der Ausdruck
(in den freien Variablen )
-
(bei inhaltlicher Interpretation)
genau dann wahr, wenn
und
für
ist. Der Ausdruck
(in den freien Variablen )
-
ist genau dann wahr, wenn
und
für
ist.
Somit besagt der Ausdruck
-
dass das Programm mit der Startkonfiguration anhält und dabei die Konfiguration erreicht.