YES(?,O(n^1)) 721.00/297.10 YES(?,O(n^1)) 721.00/297.10 721.00/297.10 We are left with following problem, upon which TcT provides the 721.00/297.10 certificate YES(?,O(n^1)). 721.00/297.10 721.00/297.10 Strict Trs: 721.00/297.10 { f(a(), f(x, a())) -> f(a(), f(a(), f(f(a(), a()), x))) } 721.00/297.10 Obligation: 721.00/297.10 derivational complexity 721.00/297.10 Answer: 721.00/297.10 YES(?,O(n^1)) 721.00/297.10 721.00/297.10 The problem is match-bounded by 1. The enriched problem is 721.00/297.10 compatible with the following automaton. 721.00/297.10 { f_0(1, 1) -> 1 721.00/297.10 , f_1(2, 3) -> 1 721.00/297.10 , f_1(4, 5) -> 3 721.00/297.10 , f_1(6, 1) -> 5 721.00/297.10 , f_1(6, 6) -> 9 721.00/297.10 , f_1(7, 8) -> 6 721.00/297.10 , f_1(8, 9) -> 5 721.00/297.10 , a_0() -> 1 721.00/297.10 , a_1() -> 2 721.00/297.10 , a_1() -> 4 721.00/297.10 , a_1() -> 7 721.00/297.10 , a_1() -> 8 } 721.00/297.10 721.00/297.10 Hurray, we answered YES(?,O(n^1)) 721.00/297.18 EOF