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