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.