YES(?,O(n^1)) 0.00/0.22 YES(?,O(n^1)) 0.00/0.22 0.00/0.22 We are left with following problem, upon which TcT provides the 0.00/0.22 certificate YES(?,O(n^1)). 0.00/0.22 0.00/0.22 Strict Trs: 0.00/0.22 { rev(a()) -> a() 0.00/0.22 , rev(b()) -> b() 0.00/0.22 , rev(++(x, x)) -> rev(x) 0.00/0.22 , rev(++(x, y)) -> ++(rev(y), rev(x)) } 0.00/0.22 Obligation: 0.00/0.22 innermost runtime complexity 0.00/0.22 Answer: 0.00/0.22 YES(?,O(n^1)) 0.00/0.22 0.00/0.22 The problem is match-bounded by 1. The enriched problem is 0.00/0.22 compatible with the following automaton. 0.00/0.22 { rev_0(2) -> 1 0.00/0.22 , rev_0(3) -> 1 0.00/0.22 , rev_0(4) -> 1 0.00/0.22 , rev_1(2) -> 1 0.00/0.22 , rev_1(3) -> 1 0.00/0.22 , rev_1(4) -> 1 0.00/0.22 , a_0() -> 2 0.00/0.22 , a_1() -> 1 0.00/0.22 , b_0() -> 3 0.00/0.22 , b_1() -> 1 0.00/0.22 , ++_0(2, 2) -> 4 0.00/0.22 , ++_0(2, 3) -> 4 0.00/0.22 , ++_0(2, 4) -> 4 0.00/0.22 , ++_0(3, 2) -> 4 0.00/0.22 , ++_0(3, 3) -> 4 0.00/0.22 , ++_0(3, 4) -> 4 0.00/0.22 , ++_0(4, 2) -> 4 0.00/0.22 , ++_0(4, 3) -> 4 0.00/0.22 , ++_0(4, 4) -> 4 0.00/0.22 , ++_1(1, 1) -> 1 } 0.00/0.22 0.00/0.22 Hurray, we answered YES(?,O(n^1)) 0.00/0.22 EOF