Registermaschine/Einzelbefehle/Arithmetische Repräsentierung/Fakt

Arithmetische Repräsentierung von Registerbefehlen

Die Programmzeilen eines Registerprogramms mit ${}m$ Registern bzw. die zugehörige Programmabbildung lassen sich folgendermaßen mit den Variablen ${}z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}$ arithmetisch repräsentieren (dabei sei ${}\ell$ die aktuelle Programmzeile).

1. ${}B_{\ell }=i+$ wird arithmetisiert durch

   $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})).$

2. ${}B_{\ell }=i-$ wird arithmetisiert durch

   $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})).$

3. ${}B_{\ell }=C(i,j)$ wird arithmetisiert durch

   $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})).$

4. ${}B_{\ell }=B_{h}=H$ wird arithmetisiert durch

   $A_{h}:=((z=h)\rightarrow (z'=h)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m})).$

Zum Beweis, Alternativen Beweis erstellen