0 :: a
add :: a → a → a
fact :: a → a
mult :: a → a → a
rec :: (a → a → a) → a → a → a
s :: a → a
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))