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