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)) Usable Rule Processor: DPs: fib#(s(s(x))) -> fib#(x) fib#(s(s(x))) -> fib#(s(x)) TRS: Restore Modifier: 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)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [fib#](x0) = x0, [+](x0, x1) = 0, [s](x0) = x0 + 1, [fib](x0) = 1, [0] = 0 orientation: fib#(s(s(x))) = x + 2 >= x = fib#(x) fib#(s(s(x))) = x + 2 >= x + 1 = fib#(s(x)) fib(0()) = 1 >= 0 = 0() fib(s(0())) = 1 >= 1 = s(0()) fib(s(s(x))) = 1 >= 0 = +(fib(s(x)),fib(x)) problem: DPs: TRS: fib(0()) -> 0() fib(s(0())) -> s(0()) fib(s(s(x))) -> +(fib(s(x)),fib(x)) Qed