Es sei
eine
-entscheidbare Relation
und es sei
ein
Registerprogramm
mit den Registern
das diese Relation entscheidet. Aufgrund von
Fakt
gibt es einen arithmetischen Ausdruck
in
freien Variablen, der den Programmablauf arithmetisch modelliert. Es gilt also
genau dann, wenn
, angesetzt auf
(strenggenommen angesetzt auf
, wenn man die vollständige Registerbelegung angibt)
anhält mit der Ausgabe
(d.h.
; andernfalls wird mit der Ausgabe
angehalten),
genau dann, wenn
gilt.
Wegen der Vollständigkeit von
bedeutet dies, dass
-

die Relation
repräsentiert.
Es sei
-
eine
-berechenbare Abbildung
und es sei
ein
Registerprogramm,
dass
berechnet. Aufgrund von
Fakt
gibt es einen arithmetischen Ausdruck
in
freien Variablen, der den Programmablauf arithmetisch modelliert. D.h. für jedes
-Tupel
gilt
-

genau dann, wenn das Programm
bei jeder Eingabe anhält und angesetzt auf
(in den ersten
Registern, die Eingabe ist also
)
die Ausgabe
(also
)
besitzt, genau dann, wenn
-
gilt. Von daher ist der Ausdruck
(in den freien Variablen
)
-

Da eine Funktion vorliegt und
vollständig ist, gilt auch
-