Alphabet

0:a
add:[a × a] ⟶ a
fact:a → a
mult:a → a → a
rec:[a → a → a × a] ⟶ a → a
s:[a] ⟶ a

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
F1:a → a → a
Y1:a
G1:a → a → a
V1:a
W1:a

Rules

add(0, X)⇒X
add(s(Y), U)⇒s(add(Y, U))
mult · 0 · V⇒0
mult · s(W) · P⇒add(mult · W · P, P)
rec(F1, Y1) · 0⇒Y1
rec(G1, V1) · s(W1)⇒G1 · s(W1) · (rec(G1, V1) · W1)
fact⇒rec(mult, s(0))