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