YES(?,O(n^1)) 866.31/297.02 YES(?,O(n^1)) 866.31/297.02 866.31/297.02 We are left with following problem, upon which TcT provides the 866.31/297.02 certificate YES(?,O(n^1)). 866.31/297.02 866.31/297.02 Strict Trs: 866.31/297.02 { f(x, f(y, a())) -> f(f(f(f(a(), a()), y), h(a())), x) } 866.31/297.02 Obligation: 866.31/297.02 derivational complexity 866.31/297.02 Answer: 866.31/297.02 YES(?,O(n^1)) 866.31/297.02 866.31/297.02 The problem is match-bounded by 2. The enriched problem is 866.31/297.02 compatible with the following automaton. 866.31/297.02 { f_0(1, 1) -> 1 866.31/297.02 , f_1(2, 1) -> 1 866.31/297.02 , f_1(2, 2) -> 1 866.31/297.02 , f_1(2, 5) -> 3 866.31/297.02 , f_1(3, 4) -> 2 866.31/297.02 , f_1(5, 1) -> 3 866.31/297.02 , f_1(5, 2) -> 3 866.31/297.02 , f_1(6, 7) -> 5 866.31/297.02 , f_2(9, 2) -> 3 866.31/297.02 , f_2(10, 11) -> 9 866.31/297.02 , f_2(12, 6) -> 10 866.31/297.02 , f_2(13, 14) -> 12 866.31/297.02 , a_0() -> 1 866.31/297.02 , a_1() -> 6 866.31/297.02 , a_1() -> 7 866.31/297.02 , a_1() -> 8 866.31/297.02 , a_2() -> 13 866.31/297.02 , a_2() -> 14 866.31/297.02 , a_2() -> 15 866.31/297.02 , h_0(1) -> 1 866.31/297.02 , h_1(8) -> 4 866.31/297.02 , h_2(15) -> 11 } 866.31/297.02 866.31/297.02 Hurray, we answered YES(?,O(n^1)) 866.44/297.19 EOF