We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { from(X) -> cons(X, n__from(n__s(X))) , from(X) -> n__from(X) , cons(X1, X2) -> n__cons(X1, X2) , 2ndspos(0(), Z) -> rnil() , 2ndspos(s(N), cons(X, n__cons(Y, Z))) -> rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z))) , s(X) -> n__s(X) , activate(X) -> X , activate(n__from(X)) -> from(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , 2ndsneg(0(), Z) -> rnil() , 2ndsneg(s(N), cons(X, n__cons(Y, Z))) -> rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z))) , pi(X) -> 2ndspos(X, from(0())) , plus(0(), Y) -> Y , plus(s(X), Y) -> s(plus(X, Y)) , times(0(), Y) -> 0() , times(s(X), Y) -> plus(Y, times(X, Y)) , square(X) -> times(X, X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Arguments of following rules are not normal-forms: { 2ndspos(s(N), cons(X, n__cons(Y, Z))) -> rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z))) , 2ndsneg(s(N), cons(X, n__cons(Y, Z))) -> rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z))) , plus(s(X), Y) -> s(plus(X, Y)) , times(s(X), Y) -> plus(Y, times(X, Y)) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { from(X) -> cons(X, n__from(n__s(X))) , from(X) -> n__from(X) , cons(X1, X2) -> n__cons(X1, X2) , 2ndspos(0(), Z) -> rnil() , s(X) -> n__s(X) , activate(X) -> X , activate(n__from(X)) -> from(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , 2ndsneg(0(), Z) -> rnil() , pi(X) -> 2ndspos(X, from(0())) , plus(0(), Y) -> Y , times(0(), Y) -> 0() , square(X) -> times(X, X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1}, safe(n__s) = {1}, safe(2ndspos) = {1, 2}, safe(0) = {}, safe(rnil) = {}, safe(s) = {1}, safe(n__cons) = {1, 2}, safe(activate) = {}, safe(2ndsneg) = {}, safe(pi) = {}, safe(plus) = {}, safe(times) = {1, 2}, safe(square) = {} and precedence from > cons, activate > from, activate > cons, activate > s, pi > from, pi > 2ndspos, square > times . Following symbols are considered recursive: {activate} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: from(; X) > cons(; X, n__from(; n__s(; X))) from(; X) > n__from(; X) cons(; X1, X2) > n__cons(; X1, X2) 2ndspos(; 0(), Z) > rnil() s(; X) > n__s(; X) activate(X;) > X activate(n__from(; X);) > from(; activate(X;)) activate(n__s(; X);) > s(; activate(X;)) activate(n__cons(; X1, X2);) > cons(; activate(X1;), X2) 2ndsneg(0(), Z;) > rnil() pi(X;) > 2ndspos(; X, from(; 0())) plus(0(), Y;) > Y times(; 0(), Y) > 0() square(X;) > times(; X, X) Hurray, we answered YES(?,O(n^1))