(VAR x y z) (RULES fib(0) -> 0 fib(s(0)) -> s(0) fib(s(s(x))) -> +(fib(s(x)),fib(x)) ) (COMMENT Example 2.24 (Fibonacci Function) in \cite{SK90})