YES(?,O(n^1)) 5.38/1.64 YES(?,O(n^1)) 5.38/1.64 5.38/1.64 We are left with following problem, upon which TcT provides the 5.38/1.64 certificate YES(?,O(n^1)). 5.38/1.64 5.38/1.64 Strict Trs: 5.38/1.64 { f(a()) -> f(c(a())) 5.38/1.64 , f(a()) -> f(d(a())) 5.38/1.64 , f(c(X)) -> X 5.38/1.64 , f(c(a())) -> f(d(b())) 5.38/1.64 , f(c(b())) -> f(d(a())) 5.38/1.64 , f(d(X)) -> X 5.38/1.64 , e(g(X)) -> e(X) } 5.38/1.64 Obligation: 5.38/1.64 derivational complexity 5.38/1.64 Answer: 5.38/1.64 YES(?,O(n^1)) 5.38/1.64 5.38/1.64 The problem is match-bounded by 2. The enriched problem is 5.38/1.64 compatible with the following automaton. 5.38/1.64 { f_0(1) -> 1 5.38/1.64 , f_1(2) -> 1 5.38/1.64 , f_2(4) -> 1 5.38/1.64 , a_0() -> 1 5.38/1.64 , a_1() -> 1 5.38/1.64 , a_1() -> 3 5.38/1.64 , a_2() -> 1 5.38/1.64 , a_2() -> 5 5.38/1.64 , c_0(1) -> 1 5.38/1.64 , c_1(3) -> 2 5.38/1.64 , d_0(1) -> 1 5.38/1.64 , d_1(3) -> 2 5.38/1.64 , d_2(5) -> 4 5.38/1.64 , b_0() -> 1 5.38/1.64 , b_1() -> 1 5.38/1.64 , b_1() -> 3 5.38/1.64 , b_2() -> 1 5.38/1.64 , b_2() -> 5 5.38/1.64 , e_0(1) -> 1 5.38/1.64 , e_1(1) -> 1 5.38/1.64 , g_0(1) -> 1 } 5.38/1.64 5.38/1.64 Hurray, we answered YES(?,O(n^1)) 5.38/1.65 EOF