Alphabet
0
:
a
id
:
a → a
plus
:
[a] ⟶ a → a
s
:
[a] ⟶ a
Variables
X
:
a
Y
:
a
U
:
a
Rules
id
·
X
⇒
X
plus
(
0
)
⇒
id
plus
(
s
(
Y
)) ·
U
⇒
s
(
plus
(
Y
) ·
U
)