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