YES(?,O(n^1)) 1178.31/297.04 YES(?,O(n^1)) 1178.31/297.04 1178.31/297.04 We are left with following problem, upon which TcT provides the 1178.31/297.04 certificate YES(?,O(n^1)). 1178.31/297.04 1178.31/297.04 Strict Trs: 1178.31/297.04 { a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1))))))))) } 1178.31/297.04 Obligation: 1178.31/297.04 derivational complexity 1178.31/297.04 Answer: 1178.31/297.04 YES(?,O(n^1)) 1178.31/297.04 1178.31/297.04 The problem is match-bounded by 3. The enriched problem is 1178.31/297.04 compatible with the following automaton. 1178.31/297.04 { a_0(1) -> 1 1178.31/297.04 , a_1(2) -> 1 1178.31/297.04 , a_1(2) -> 7 1178.31/297.04 , a_1(2) -> 34 1178.31/297.04 , a_1(4) -> 3 1178.31/297.04 , a_1(5) -> 4 1178.31/297.04 , a_1(7) -> 6 1178.31/297.04 , a_1(8) -> 7 1178.31/297.04 , a_1(9) -> 8 1178.31/297.04 , a_2(13) -> 7 1178.31/297.04 , a_2(13) -> 34 1178.31/297.04 , a_2(13) -> 61 1178.31/297.04 , a_2(15) -> 14 1178.31/297.04 , a_2(16) -> 15 1178.31/297.04 , a_2(18) -> 17 1178.31/297.04 , a_2(19) -> 18 1178.31/297.04 , a_2(20) -> 19 1178.31/297.04 , a_2(21) -> 3 1178.31/297.04 , a_2(21) -> 30 1178.31/297.04 , a_2(23) -> 22 1178.31/297.04 , a_2(24) -> 23 1178.31/297.04 , a_2(26) -> 25 1178.31/297.04 , a_2(27) -> 26 1178.31/297.04 , a_2(28) -> 27 1178.31/297.04 , a_2(29) -> 6 1178.31/297.04 , a_2(29) -> 33 1178.31/297.04 , a_2(31) -> 30 1178.31/297.04 , a_2(32) -> 31 1178.31/297.04 , a_2(34) -> 33 1178.31/297.04 , a_2(35) -> 34 1178.31/297.04 , a_2(36) -> 35 1178.31/297.04 , a_3(48) -> 30 1178.31/297.04 , a_3(48) -> 57 1178.31/297.04 , a_3(50) -> 49 1178.31/297.04 , a_3(51) -> 50 1178.31/297.04 , a_3(53) -> 52 1178.31/297.04 , a_3(54) -> 53 1178.31/297.04 , a_3(55) -> 54 1178.31/297.04 , a_3(56) -> 33 1178.31/297.04 , a_3(56) -> 60 1178.31/297.04 , a_3(58) -> 57 1178.31/297.04 , a_3(59) -> 58 1178.31/297.04 , a_3(61) -> 60 1178.31/297.04 , a_3(62) -> 61 1178.31/297.04 , a_3(63) -> 62 1178.31/297.04 , b_0(1) -> 1 1178.31/297.04 , b_1(1) -> 9 1178.31/297.04 , b_1(2) -> 9 1178.31/297.04 , b_1(3) -> 2 1178.31/297.04 , b_1(4) -> 9 1178.31/297.04 , b_1(6) -> 5 1178.31/297.04 , b_1(7) -> 9 1178.31/297.04 , b_1(21) -> 9 1178.31/297.04 , b_1(29) -> 9 1178.31/297.04 , b_2(2) -> 20 1178.31/297.04 , b_2(4) -> 28 1178.31/297.04 , b_2(5) -> 20 1178.31/297.04 , b_2(7) -> 36 1178.31/297.04 , b_2(8) -> 20 1178.31/297.04 , b_2(9) -> 20 1178.31/297.04 , b_2(13) -> 20 1178.31/297.04 , b_2(14) -> 13 1178.31/297.04 , b_2(15) -> 28 1178.31/297.04 , b_2(17) -> 16 1178.31/297.04 , b_2(18) -> 36 1178.31/297.04 , b_2(21) -> 28 1178.31/297.04 , b_2(22) -> 21 1178.31/297.04 , b_2(25) -> 24 1178.31/297.04 , b_2(29) -> 36 1178.31/297.04 , b_2(30) -> 29 1178.31/297.04 , b_2(33) -> 32 1178.31/297.04 , b_3(15) -> 55 1178.31/297.04 , b_3(18) -> 63 1178.31/297.04 , b_3(49) -> 48 1178.31/297.04 , b_3(52) -> 51 1178.31/297.04 , b_3(57) -> 56 1178.31/297.04 , b_3(60) -> 59 } 1178.31/297.04 1178.31/297.04 Hurray, we answered YES(?,O(n^1)) 1179.00/297.62 EOF