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