Arithmetische Repräsentierung von Registerbefehlen
Die Programmzeilen eines Registerprogramms mit
m
{\displaystyle {}m}
z
,
r
1
,
…
,
r
m
,
z
′
,
r
1
′
,
…
,
r
m
′
{\displaystyle {}z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}}
ℓ
{\displaystyle {}\ell }
B
ℓ
=
i
+
{\displaystyle {}B_{\ell }=i+}
A
ℓ
:=
(
(
z
=
ℓ
)
→
(
z
′
=
z
+
1
)
∧
(
r
1
′
=
r
1
)
∧
…
∧
(
r
i
−
1
′
=
r
i
−
1
)
∧
(
r
i
′
=
r
i
+
1
)
∧
(
r
i
+
1
′
=
r
i
+
1
)
∧
…
∧
(
r
m
′
=
r
m
)
)
.
{\displaystyle 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})).}
B
ℓ
=
i
−
{\displaystyle {}B_{\ell }=i-}
A
ℓ
:=
(
(
z
=
ℓ
)
→
(
z
′
=
z
+
1
)
∧
(
r
1
′
=
r
1
)
∧
…
∧
(
r
i
−
1
′
=
r
i
−
1
)
∧
(
(
r
i
=
0
)
→
r
i
′
=
r
i
)
∧
(
¬
(
r
i
=
0
)
→
r
i
′
+
1
=
r
i
)
∧
(
r
i
+
1
′
=
r
i
+
1
)
∧
…
∧
(
r
m
′
=
r
m
)
)
.
{\displaystyle 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})).}
B
ℓ
=
C
(
i
,
j
)
{\displaystyle {}B_{\ell }=C(i,j)}
A
ℓ
:=
(
(
z
=
ℓ
)
→
(
(
r
i
=
0
→
(
z
′
=
j
)
)
∧
(
¬
(
r
i
=
0
)
→
(
z
′
=
z
+
1
)
)
)
∧
(
r
1
′
=
r
1
)
∧
…
∧
(
r
m
′
=
r
m
)
)
.
{\displaystyle 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})).}
B
ℓ
=
B
h
=
H
{\displaystyle {}B_{\ell }=B_{h}=H}
A
h
:=
(
(
z
=
h
)
→
(
z
′
=
h
)
∧
(
r
1
′
=
r
1
)
∧
…
∧
(
r
m
′
=
r
m
)
)
.
{\displaystyle A_{h}:=((z=h)\rightarrow (z'=h)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m})).}
