YES(?,O(n^1)) 840.34/297.03 YES(?,O(n^1)) 840.34/297.03 840.34/297.03 We are left with following problem, upon which TcT provides the 840.34/297.03 certificate YES(?,O(n^1)). 840.34/297.03 840.34/297.03 Strict Trs: 840.34/297.03 { f(f(a(), x), a()) -> f(f(f(x, f(a(), a())), a()), a()) } 840.34/297.03 Obligation: 840.34/297.03 derivational complexity 840.34/297.03 Answer: 840.34/297.03 YES(?,O(n^1)) 840.34/297.03 840.34/297.03 We uncurry the input using the following uncurry rules. 840.34/297.03 840.34/297.03 { f(a(), x_1) -> a_1(x_1) 840.34/297.03 , f(a_1(x_1), x_2) -> a_2(x_1, x_2) } 840.34/297.03 840.34/297.03 We are left with following problem, upon which TcT provides the 840.34/297.03 certificate YES(?,O(n^1)). 840.34/297.03 840.34/297.03 Strict Trs: { a_2(x, a()) -> f(f(f(x, a_1(a())), a()), a()) } 840.34/297.03 Weak Trs: 840.34/297.03 { f(a(), x_1) -> a_1(x_1) 840.34/297.03 , f(a_1(x_1), x_2) -> a_2(x_1, x_2) } 840.34/297.03 Obligation: 840.34/297.03 derivational complexity 840.34/297.03 Answer: 840.34/297.03 YES(?,O(n^1)) 840.34/297.03 840.34/297.03 The problem is match-bounded by 2. The enriched problem is 840.34/297.03 compatible with the following automaton. 840.34/297.03 { f_0(1, 1) -> 1 840.34/297.03 , f_1(1, 6) -> 4 840.34/297.03 , f_1(2, 3) -> 1 840.34/297.03 , f_1(4, 5) -> 2 840.34/297.03 , f_2(6, 12) -> 10 840.34/297.03 , f_2(8, 9) -> 2 840.34/297.03 , f_2(10, 11) -> 8 840.34/297.03 , a_2_0(1, 1) -> 1 840.34/297.03 , a_2_1(1, 6) -> 4 840.34/297.03 , a_2_1(6, 5) -> 2 840.34/297.03 , a_2_2(7, 12) -> 10 840.34/297.03 , a_0() -> 1 840.34/297.03 , a_1() -> 3 840.34/297.03 , a_1() -> 5 840.34/297.03 , a_1() -> 7 840.34/297.03 , a_2() -> 9 840.34/297.03 , a_2() -> 11 840.34/297.03 , a_2() -> 13 840.34/297.03 , a_1_0(1) -> 1 840.34/297.03 , a_1_1(6) -> 4 840.34/297.03 , a_1_1(7) -> 6 840.34/297.03 , a_1_2(13) -> 12 } 840.34/297.03 840.34/297.03 Hurray, we answered YES(?,O(n^1)) 840.49/297.16 EOF