# Registermaschine/Einzelbefehle/Arithmetische Repräsentierung/Textabschnitt
## Definition

Den Programmzeilen $B_{1},\ldots ,B_{h}$ eines Registerprogramms mit $m$ Registern werden die folgenden arithmetischen Ausdrücke $A_{1},\ldots ,A_{h}$ in den freien Variablen $z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}$ zugeordnet.
* Bei $B_{\ell }=i+$ setzt man
    $A_{\ell }:=(z=\ell )\rightarrow (z'=z+1)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{i-1}'=r_{i-1})\wedge (r_{i}'=r_{i}+1)\wedge (r_{i+1}'=r_{i+1})\wedge \ldots \wedge (r_{m}'=r_{m}).$
* Bei $B_{\ell }=i-$ setzt man
    $A_{\ell }:=(z=\ell )\rightarrow (z'=z+1)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{i-1}'=r_{i-1})\wedge ((r_{i}=0)\rightarrow (r'_{i}=r_{i}))\wedge (\neg (r_{i}=0)\rightarrow (r_{i}'+1=r_{i}))\wedge (r_{i+1}'=r_{i+1})\wedge \ldots \wedge (r_{m}'=r_{m}).$
* Bei $B_{\ell }=C(ij)$ setzt man
    $A_{\ell }:=(z=\ell )\rightarrow ((r_{i}=0)\rightarrow (z'=j))\wedge (\neg (r_{i}=0)\rightarrow (z'=z+1))\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m}).$
* Bei $B_{\ell }=B_{h}=H$ setzt man
    $A_{h}:=(z=h)\rightarrow (z'=z)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m}).$
Hierbei werden die natürlichen Zahlen $\ell$ und $j$ in den arithmetischen Ausdrücken durch die entsprechenden Summen $1+\cdots +1$ repräsentiert, die Abfrage am $i$-ten Register schlägt sich in der Variablenbezeichnung nieder.
Wie bei der Programmabbildung ist es sinnvoll, für alle Programmzeilennummern (also auch für $\ell >h$) einen arithmetischen Ausdruck zu haben. Dazu setzen wir
    $A_{h+1}:=(z\geq h+1)\rightarrow (z'=z)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m})$
(wobei $z\geq h+1$ eine Abkürzung ist). Zu einem gegebenen Programm bestehend aus den Programmzeilen $B_{1},\ldots ,B_{h}$ betrachtet man die Konjunktion der soeben eingeführten zugehörigen arithmetischen Repräsentierungen, also $A_{P}=A_{1}\wedge A_{2}\wedge \ldots \wedge A_{h}\wedge A_{h+1}$. Dieser Ausdruck repräsentiert die Programmabbildung.

## Lemma

Es sei $P$ ein Registerprogramm mit den Programmzeilen $B_{1},\ldots ,B_{h}$ und $m$ Registern mit den zugehörigen arithmetischen Ausdrücken $A_{1},\ldots ,A_{h}$ in den freien Variablen $z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}$. Es sei $A_{P}=A_{1}\wedge \ldots \wedge A_{h}\wedge A_{h+1}$.
Dann ist $A_{P}$ eine arithmetische Repräsentierung der Programmabbildung $\varphi _{P}$.

### Beweis

Die Variablen $z,z',r_{j},r_{j}'$ seien durch die natürlichen Zahlen $\ell ,\ell ',n_{j},n_{j}'$ belegt. Wir müssen zeigen, dass die Gleichheit
    $\varphi _{P}(\ell ,n_{1},\ldots ,n_{m})=(\ell ',n'_{1},\ldots ,n'_{m})\,$
genau dann gilt, wenn
    $\mathbb {N} \vDash A_{P}(\ell ,\ell ',n_{1},\ldots ,n_{m},n'_{1},\ldots ,n'_{m})$
gilt. Der Ausdruck $A_{P}$ gilt genau dann, wenn sämtliche Ausdrücke $A_{1},A_{2},\ldots ,A_{h},A_{h+1}$ gelten. Es sei $\ell$ fixiert. Dann gelten sämtliche $A_{k}$, $k\neq \ell$, automatisch, da für diese Ausdrücke der Vordersatz nicht gilt. Die Gültigkeit von $A_{P}$ bei dieser Belegung bedeutet also, dass der Nachsatz in $A_{\ell }$ gelten muss. Sowohl $\varphi (\ell ,-)$ als auch der Nachsatz von $A_{\ell }$ drücken die Wirkungsweise des Befehls $B_{\ell }$ aus, daher gilt die Abbildungsgleichheit genau dann, wenn $A_{\ell }$ wahr ist.
$\Box$