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