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