Alphabet

0:a
add:a → a → a
curry:[a → a → a] ⟶ a → a → a
plus:a → a → a
s:[a] ⟶ a

Variables

X:a
Y:a
U:a
H:a → a → a
W:a
P:a

Rules

plus · 0 · XX
plus · s(Y) · Us(plus · Y · U)
curry(H) · W · PH · W · P
addcurry(plus)