Alphabet

0:a
comp:[b → b × b → b] ⟶ b → b
plus:[a × a] ⟶ a
s:[a] ⟶ a
times:[a × a] ⟶ a
twice:[b → b] ⟶ b → b

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
F1:b → b
Z1:b → b
U1:b
H1:b → b

Rules

plus(0, X)⇒X
plus(s(Y), U)⇒s(plus(Y, U))
times(0, V)⇒0
times(s(W), P)⇒plus(times(W, P), P)
comp(F1, Z1) · U1⇒F1 · (Z1 · U1)
twice(H1)⇒comp(H1, H1)