TRS: { fib(0()) -> 0(), fib(s(0())) -> s(0()), fib(s(s(x))) -> +(fib(s(x)), fib(x))} LMPO: Quasi-Precedence: empty Normal: pi(fib) = [1] Safe: Predicative System: { fib(0();) -> 0(), fib(s(0(););) -> s(0();), fib(s(s(x;););) -> +(fib(s(x;);),fib(x;);)} Qed