YES Problem: fib(0()) -> 0() fib(s(0())) -> s(0()) fib(s(s(x))) -> +(fib(s(x)),fib(x)) Proof: DP Processor: DPs: fib#(s(s(x))) -> fib#(x) fib#(s(s(x))) -> fib#(s(x)) TRS: fib(0()) -> 0() fib(s(0())) -> s(0()) fib(s(s(x))) -> +(fib(s(x)),fib(x)) Subterm Criterion Processor: simple projection: pi(fib#) = 0 problem: DPs: TRS: fib(0()) -> 0() fib(s(0())) -> s(0()) fib(s(s(x))) -> +(fib(s(x)),fib(x)) Qed