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