Alphabet
lim
:
(N → O) → O
plus
:
O → O → O
s
:
O → O
z
:
O
Variables
X
:
O
Y
:
O
U
:
O
H
:
N → O
W
:
O
Rules
plus
·
z
·
X
⇒
X
plus
· (
s
·
Y
) ·
U
⇒
s
· (
plus
·
Y
·
U
)
plus
· (
lim
· (λ
%X
:N.
H
·
%X
)) ·
W
⇒
lim
· (λ
%Y
:N.
plus
· (
H
·
%Y
) ·
W
)