Die Programmzeilen eines Registerprogramms mit Registern bzw. die zugehörige Programmabbildung lassen sich folgendermaßen mit den Variablen arithmetisch repräsentieren
(dabei sei die aktuelle Programmzeile).
Die
arithmetische Repräsentierbarkeit
der Programmabbildung bedeutet, dass
genau dann gilt, wenn die entsprechende arithmetische Aussage in gilt. Genau so wurden aber die definiert.
Zu einem gegebenen Programm bestehend aus den Programmzeilen betrachtet man die Konjunktion der soeben eingeführten zugehörigen arithmetischen Repräsentierungen, also
Die Aussage ist somit für eine Variablenbelegung
(der Variablen mit Werten in )
genau dann gültig, wenn ist
(da dann keine Bedingung der einzelnen konjugierten Aussage erfüllt ist)
oder wenn ist und erfüllt
(d.h. dass die Konklusion in erfüllt ist) ist, und dies ist nach dem Lemma genau dann der Fall, wenn die
(Variablen)-Belegung von die Programmzeilennummer ist, die durch den aktuellen
(durch die Belegung von festgelegten)
Befehl als nächste Programmzeile aufgerufen wird, und wenn die Belegungen der die aus diesem Befehl resultierenden Belegungen der sind.