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