Input TRS: 1: fib(N) -> sel(N,fib1(s(0()),s(0()))) 2: fib1(X,Y) -> cons(X,n__fib1(Y,add(X,Y))) 3: add(0(),X) -> X 4: add(s(X),Y) -> s(add(X,Y)) 5: sel(0(),cons(X,XS)) -> X 6: sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) 7: fib1(X1,X2) -> n__fib1(X1,X2) 8: activate(n__fib1(X1,X2)) -> fib1(X1,X2) 9: activate(X) -> X Number of strict rules: 9 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #fib1(X,Y) -> #add(X,Y) #2: #sel(s(N),cons(X,XS)) -> #sel(N,activate(XS)) #3: #sel(s(N),cons(X,XS)) -> #activate(XS) #4: #fib(N) -> #sel(N,fib1(s(0()),s(0()))) #5: #fib(N) -> #fib1(s(0()),s(0())) #6: #activate(n__fib1(X1,X2)) -> #fib1(X1,X2) #7: #add(s(X),Y) -> #add(X,Y) Number of SCCs: 2, DPs: 2, edges: 2 SCC { #7 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 2) + x1 activate(x1) weight: 0 #activate(x1) weight: 0 #fib1(x1,x2) weight: 0 n__fib1(x1,x2) weight: 0 fib1(x1,x2) weight: 0 fib(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 sel(x1,x2) weight: 0 cons(x1,x2) weight: 0 #add(x1,x2) weight: x1 add(x1,x2) weight: 0 #fib(x1) weight: 0 Usable rules: { } Removed DPs: #7 Number of SCCs: 1, DPs: 1, edges: 1 SCC { #2 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 4) + x1 activate(x1) weight: (/ 1 4) #activate(x1) weight: 0 #fib1(x1,x2) weight: 0 n__fib1(x1,x2) weight: (/ 3 4) fib1(x1,x2) weight: (/ 1 2) + x1 fib(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: x1 sel(x1,x2) weight: 0 cons(x1,x2) weight: (/ 1 4) + x2 #add(x1,x2) weight: 0 add(x1,x2) weight: (/ 1 4) #fib(x1) weight: 0 Usable rules: { } Removed DPs: #2 Number of SCCs: 0, DPs: 0, edges: 0 YES