Alphabet
ack
:
[N × N] ⟶ N
s
:
[N] ⟶ N
z
:
N
Variables
X
:
N
Y
:
N
U
:
N
V
:
N
Rules
ack
(
z
,
X
)
⇒
s
(
X
)
ack
(
s
(
Y
),
z
)
⇒
ack
(
Y
,
s
(
z
))
ack
(
s
(
U
),
s
(
V
))
⇒
ack
(
U
,
ack
(
s
(
U
),
V
))