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