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