YES(?,O(n^1)) 444.66/209.77 YES(?,O(n^1)) 444.66/209.77 444.66/209.77 We are left with following problem, upon which TcT provides the 444.66/209.77 certificate YES(?,O(n^1)). 444.66/209.77 444.66/209.77 Strict Trs: 444.66/209.77 { 0(1(2(3(4(x1))))) -> 0(2(1(3(4(x1))))) 444.66/209.77 , 0(5(1(2(4(3(x1)))))) -> 0(5(2(1(4(3(x1)))))) 444.66/209.77 , 0(5(2(4(1(3(x1)))))) -> 0(1(5(2(4(3(x1)))))) 444.66/209.77 , 0(5(3(1(2(4(x1)))))) -> 0(1(5(3(2(4(x1)))))) 444.66/209.77 , 0(5(4(1(3(2(x1)))))) -> 0(5(4(3(1(2(x1)))))) } 444.66/209.77 Obligation: 444.66/209.77 derivational complexity 444.66/209.77 Answer: 444.66/209.77 YES(?,O(n^1)) 444.66/209.77 444.66/209.77 The problem is match-bounded by 1. The enriched problem is 444.66/209.77 compatible with the following automaton. 444.66/209.77 { 0_0(1) -> 1 444.66/209.77 , 0_0(2) -> 1 444.66/209.77 , 0_0(3) -> 1 444.66/209.77 , 0_0(4) -> 1 444.66/209.77 , 0_0(5) -> 1 444.66/209.77 , 0_0(6) -> 1 444.66/209.77 , 0_1(7) -> 1 444.66/209.77 , 1_0(1) -> 2 444.66/209.77 , 1_0(2) -> 2 444.66/209.77 , 1_0(3) -> 2 444.66/209.77 , 1_0(4) -> 2 444.66/209.77 , 1_0(5) -> 2 444.66/209.77 , 1_0(6) -> 2 444.66/209.77 , 1_1(9) -> 8 444.66/209.77 , 1_1(13) -> 12 444.66/209.77 , 1_1(15) -> 7 444.66/209.77 , 1_1(20) -> 19 444.66/209.77 , 2_0(1) -> 3 444.66/209.77 , 2_0(2) -> 3 444.66/209.77 , 2_0(3) -> 3 444.66/209.77 , 2_0(4) -> 3 444.66/209.77 , 2_0(5) -> 3 444.66/209.77 , 2_0(6) -> 3 444.66/209.77 , 2_1(1) -> 20 444.66/209.77 , 2_1(2) -> 20 444.66/209.77 , 2_1(3) -> 20 444.66/209.77 , 2_1(4) -> 20 444.66/209.77 , 2_1(5) -> 20 444.66/209.77 , 2_1(6) -> 20 444.66/209.77 , 2_1(8) -> 7 444.66/209.77 , 2_1(10) -> 17 444.66/209.77 , 2_1(12) -> 11 444.66/209.77 , 2_1(13) -> 16 444.66/209.77 , 3_0(1) -> 4 444.66/209.77 , 3_0(2) -> 4 444.66/209.77 , 3_0(3) -> 4 444.66/209.77 , 3_0(4) -> 4 444.66/209.77 , 3_0(5) -> 4 444.66/209.77 , 3_0(6) -> 4 444.66/209.77 , 3_1(1) -> 14 444.66/209.77 , 3_1(2) -> 14 444.66/209.77 , 3_1(3) -> 14 444.66/209.77 , 3_1(4) -> 14 444.66/209.77 , 3_1(5) -> 14 444.66/209.77 , 3_1(6) -> 14 444.66/209.77 , 3_1(10) -> 9 444.66/209.77 , 3_1(17) -> 16 444.66/209.77 , 3_1(19) -> 18 444.66/209.77 , 4_0(1) -> 5 444.66/209.77 , 4_0(2) -> 5 444.66/209.77 , 4_0(3) -> 5 444.66/209.77 , 4_0(4) -> 5 444.66/209.77 , 4_0(5) -> 5 444.66/209.77 , 4_0(6) -> 5 444.66/209.77 , 4_1(1) -> 10 444.66/209.77 , 4_1(2) -> 10 444.66/209.77 , 4_1(3) -> 10 444.66/209.77 , 4_1(4) -> 10 444.66/209.77 , 4_1(5) -> 10 444.66/209.77 , 4_1(6) -> 10 444.66/209.77 , 4_1(14) -> 13 444.66/209.77 , 4_1(18) -> 11 444.66/209.77 , 5_0(1) -> 6 444.66/209.77 , 5_0(2) -> 6 444.66/209.77 , 5_0(3) -> 6 444.66/209.77 , 5_0(4) -> 6 444.66/209.77 , 5_0(5) -> 6 444.66/209.77 , 5_0(6) -> 6 444.66/209.77 , 5_1(11) -> 7 444.66/209.77 , 5_1(16) -> 15 } 444.66/209.77 444.66/209.77 Hurray, we answered YES(?,O(n^1)) 444.93/209.85 EOF