Alphabet

NIL:A
in:N → (N → A) → A
new:(N → A) → A
out:N → N → A → A
sum:A → A → A
tau:A → A

Variables

X:A
Y:A
G:N → A
H:N → A
W:N
J:N → A
X1:N
Y1:N
G1:N → A
V1:N
I1:N → N → A
J1:N → A
F2:N → N → A

Rules

sum · NIL · X⇒X
new · (λ%X:N.Y)⇒Y
new · (λ%Y:N.sum · (G · %Y) · (H · %Y))⇒sum · (new · (λ%U:N.G · %U)) · (new · (λ%Z:N.H · %Z))
new · (λ%V:N.out · %V · W · (J · %V))⇒NIL
new · (λ%W:N.out · X1 · Y1 · (G1 · %W))⇒out · X1 · Y1 · (new · (λ%F:N.G1 · %F))
new · (λ%H:N.in · V1 · (λ%G:N.I1 · %H · %G))⇒in · V1 · (λ%I:N.new · (λ%J:N.I1 · %J · %I))
new · (λ%P:N.tau · (J1 · %P))⇒tau · (new · (λ%Q:N.J1 · %Q))
new · (λ%S:N.in · %S · (λ%R:N.F2 · %S · %R))⇒NIL