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