(VAR x y z)
(RULES
fac(0) -> 1
fac(s(x)) -> *(s(x),fac(x))
floop(0,y) -> y
floop(s(x),y) -> floop(x,*(s(x),y))
*(x,0) -> 0
*(x,s(y)) -> +(*(x,y),x)
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
1 -> s(0)
fac(0) -> s(0)
)
(COMMENT Example 2.23 (Factorial Function) in \cite{SK90})