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