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