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