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