(VAR x y z)
(RULES
fib(0) -> 0
fib(s(0)) -> s(0)
fib(s(s(0))) -> s(0)
fib(s(s(x))) -> sp(g(x))
g(0) -> pair(s(0),0)
g(s(0)) -> pair(s(0),s(0))
g(s(x)) -> np(g(x))
sp(pair(x,y)) -> +(x,y)
np(pair(x,y)) -> pair(+(x,y),x)
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
)

(COMMENT Example 2.27 (Fibonacci Function) in \cite{SK90})