YES(?,O(n^1)) 922.13/297.04 YES(?,O(n^1)) 922.13/297.04 922.13/297.04 We are left with following problem, upon which TcT provides the 922.13/297.04 certificate YES(?,O(n^1)). 922.13/297.04 922.13/297.04 Strict Trs: 922.13/297.04 { 0(0(4(x1))) -> 1(1(5(2(3(4(x1)))))) 922.13/297.04 , 0(4(x1)) -> 0(1(4(2(3(3(x1)))))) 922.13/297.04 , 0(4(x1)) -> 0(2(1(4(3(4(x1)))))) 922.13/297.04 , 0(4(0(x1))) -> 0(1(2(1(0(3(x1)))))) 922.13/297.04 , 0(1(1(x1))) -> 0(2(2(1(1(1(x1)))))) 922.13/297.04 , 0(1(3(x1))) -> 0(2(4(3(4(4(x1)))))) 922.13/297.04 , 0(2(4(x1))) -> 1(5(4(3(4(4(x1)))))) 922.13/297.04 , 4(0(0(x1))) -> 2(5(2(1(1(1(x1)))))) 922.13/297.04 , 4(0(5(x1))) -> 4(1(4(5(1(4(x1)))))) 922.13/297.04 , 4(0(5(x1))) -> 4(2(1(4(3(5(x1)))))) 922.13/297.04 , 1(2(3(x1))) -> 5(1(4(1(4(4(x1)))))) 922.13/297.04 , 1(3(3(x1))) -> 0(2(1(1(0(5(x1)))))) 922.13/297.04 , 1(3(3(x1))) -> 5(4(0(3(2(3(x1)))))) 922.13/297.04 , 1(3(5(x1))) -> 1(1(4(3(3(2(x1)))))) 922.13/297.04 , 2(0(0(x1))) -> 2(4(3(4(4(4(x1)))))) 922.13/297.04 , 2(0(4(x1))) -> 2(0(2(1(4(3(x1)))))) 922.13/297.04 , 2(0(4(x1))) -> 2(4(1(4(3(1(x1)))))) 922.13/297.04 , 2(0(1(x1))) -> 2(4(3(5(2(3(x1)))))) 922.13/297.04 , 2(0(1(x1))) -> 2(1(5(1(0(1(x1)))))) 922.13/297.04 , 3(0(1(x1))) -> 3(1(4(3(4(1(x1)))))) 922.13/297.04 , 3(0(5(x1))) -> 3(1(0(2(3(2(x1)))))) 922.13/297.04 , 5(0(4(x1))) -> 1(0(3(2(4(4(x1)))))) 922.13/297.04 , 5(0(4(x1))) -> 1(5(1(0(3(4(x1)))))) 922.13/297.04 , 5(0(2(x1))) -> 1(5(2(1(0(2(x1)))))) } 922.13/297.04 Obligation: 922.13/297.04 derivational complexity 922.13/297.04 Answer: 922.13/297.04 YES(?,O(n^1)) 922.13/297.04 922.13/297.04 The problem is match-bounded by 3. The enriched problem is 922.13/297.04 compatible with the following automaton. 922.13/297.04 { 0_0(1) -> 1 922.13/297.04 , 0_1(1) -> 61 922.13/297.04 , 0_1(2) -> 3 922.13/297.04 , 0_1(5) -> 13 922.13/297.04 , 0_1(7) -> 1 922.13/297.04 , 0_1(7) -> 18 922.13/297.04 , 0_1(7) -> 61 922.13/297.04 , 0_1(7) -> 66 922.13/297.04 , 0_1(7) -> 111 922.13/297.04 , 0_1(11) -> 15 922.13/297.04 , 0_1(18) -> 61 922.13/297.04 , 0_1(26) -> 1 922.13/297.04 , 0_1(33) -> 37 922.13/297.04 , 0_1(39) -> 38 922.13/297.04 , 0_1(42) -> 15 922.13/297.04 , 0_1(43) -> 1 922.13/297.04 , 0_1(43) -> 18 922.13/297.04 , 0_1(43) -> 111 922.13/297.04 , 0_1(51) -> 2 922.13/297.04 , 0_1(76) -> 13 922.13/297.04 , 0_2(1) -> 66 922.13/297.04 , 0_2(43) -> 96 922.13/297.04 , 0_2(67) -> 66 922.13/297.04 , 0_2(97) -> 96 922.13/297.04 , 0_2(98) -> 61 922.13/297.04 , 0_2(98) -> 66 922.13/297.04 , 0_2(113) -> 37 922.13/297.04 , 0_2(113) -> 61 922.13/297.04 , 0_2(113) -> 66 922.13/297.04 , 0_2(213) -> 3 922.13/297.04 , 4_0(1) -> 1 922.13/297.04 , 4_1(1) -> 6 922.13/297.04 , 4_1(2) -> 20 922.13/297.04 , 4_1(5) -> 13 922.13/297.04 , 4_1(6) -> 20 922.13/297.04 , 4_1(7) -> 6 922.13/297.04 , 4_1(9) -> 8 922.13/297.04 , 4_1(11) -> 53 922.13/297.04 , 4_1(12) -> 6 922.13/297.04 , 4_1(18) -> 71 922.13/297.04 , 4_1(19) -> 12 922.13/297.04 , 4_1(20) -> 50 922.13/297.04 , 4_1(26) -> 1 922.13/297.04 , 4_1(26) -> 6 922.13/297.04 , 4_1(26) -> 75 922.13/297.04 , 4_1(28) -> 27 922.13/297.04 , 4_1(32) -> 31 922.13/297.04 , 4_1(34) -> 6 922.13/297.04 , 4_1(36) -> 35 922.13/297.04 , 4_1(38) -> 34 922.13/297.04 , 4_1(43) -> 2 922.13/297.04 , 4_1(49) -> 2 922.13/297.04 , 4_1(51) -> 1 922.13/297.04 , 4_1(51) -> 6 922.13/297.04 , 4_1(51) -> 75 922.13/297.04 , 4_1(55) -> 54 922.13/297.04 , 4_1(68) -> 6 922.13/297.04 , 4_1(70) -> 69 922.13/297.04 , 4_1(160) -> 6 922.13/297.04 , 4_2(1) -> 75 922.13/297.04 , 4_2(12) -> 129 922.13/297.04 , 4_2(19) -> 25 922.13/297.04 , 4_2(23) -> 22 922.13/297.04 , 4_2(25) -> 24 922.13/297.04 , 4_2(26) -> 106 922.13/297.04 , 4_2(38) -> 25 922.13/297.04 , 4_2(43) -> 225 922.13/297.04 , 4_2(49) -> 25 922.13/297.04 , 4_2(51) -> 106 922.13/297.04 , 4_2(56) -> 24 922.13/297.04 , 4_2(57) -> 56 922.13/297.04 , 4_2(67) -> 75 922.13/297.04 , 4_2(68) -> 129 922.13/297.04 , 4_2(74) -> 73 922.13/297.04 , 4_2(80) -> 129 922.13/297.04 , 4_2(100) -> 99 922.13/297.04 , 4_2(105) -> 104 922.13/297.04 , 4_2(106) -> 24 922.13/297.04 , 4_2(126) -> 103 922.13/297.04 , 4_2(129) -> 128 922.13/297.04 , 4_2(162) -> 161 922.13/297.04 , 4_2(215) -> 214 922.13/297.04 , 4_2(224) -> 223 922.13/297.04 , 4_2(225) -> 24 922.13/297.04 , 4_3(57) -> 242 922.13/297.04 , 4_3(126) -> 159 922.13/297.04 , 4_3(157) -> 156 922.13/297.04 , 4_3(159) -> 158 922.13/297.04 , 4_3(240) -> 239 922.13/297.04 , 4_3(242) -> 241 922.13/297.04 , 1_0(1) -> 1 922.13/297.04 , 1_1(1) -> 18 922.13/297.04 , 1_1(2) -> 1 922.13/297.04 , 1_1(2) -> 18 922.13/297.04 , 1_1(2) -> 33 922.13/297.04 , 1_1(2) -> 61 922.13/297.04 , 1_1(2) -> 66 922.13/297.04 , 1_1(2) -> 96 922.13/297.04 , 1_1(2) -> 111 922.13/297.04 , 1_1(3) -> 2 922.13/297.04 , 1_1(6) -> 29 922.13/297.04 , 1_1(7) -> 1 922.13/297.04 , 1_1(7) -> 18 922.13/297.04 , 1_1(7) -> 111 922.13/297.04 , 1_1(8) -> 7 922.13/297.04 , 1_1(13) -> 12 922.13/297.04 , 1_1(15) -> 14 922.13/297.04 , 1_1(17) -> 16 922.13/297.04 , 1_1(18) -> 17 922.13/297.04 , 1_1(20) -> 36 922.13/297.04 , 1_1(21) -> 1 922.13/297.04 , 1_1(26) -> 18 922.13/297.04 , 1_1(27) -> 26 922.13/297.04 , 1_1(31) -> 30 922.13/297.04 , 1_1(35) -> 34 922.13/297.04 , 1_1(37) -> 13 922.13/297.04 , 1_1(43) -> 1 922.13/297.04 , 1_1(51) -> 18 922.13/297.04 , 1_1(53) -> 52 922.13/297.04 , 1_1(54) -> 49 922.13/297.04 , 1_1(61) -> 4 922.13/297.04 , 1_1(69) -> 68 922.13/297.04 , 1_2(1) -> 111 922.13/297.04 , 1_2(2) -> 112 922.13/297.04 , 1_2(3) -> 117 922.13/297.04 , 1_2(7) -> 112 922.13/297.04 , 1_2(8) -> 67 922.13/297.04 , 1_2(21) -> 1 922.13/297.04 , 1_2(21) -> 18 922.13/297.04 , 1_2(21) -> 61 922.13/297.04 , 1_2(21) -> 66 922.13/297.04 , 1_2(21) -> 96 922.13/297.04 , 1_2(21) -> 111 922.13/297.04 , 1_2(27) -> 1 922.13/297.04 , 1_2(43) -> 1 922.13/297.04 , 1_2(64) -> 56 922.13/297.04 , 1_2(66) -> 65 922.13/297.04 , 1_2(67) -> 111 922.13/297.04 , 1_2(73) -> 72 922.13/297.04 , 1_2(93) -> 3 922.13/297.04 , 1_2(93) -> 33 922.13/297.04 , 1_2(96) -> 95 922.13/297.04 , 1_2(99) -> 98 922.13/297.04 , 1_2(104) -> 103 922.13/297.04 , 1_2(111) -> 110 922.13/297.04 , 1_2(112) -> 111 922.13/297.04 , 1_2(116) -> 115 922.13/297.04 , 1_2(117) -> 116 922.13/297.04 , 1_2(128) -> 162 922.13/297.04 , 1_2(161) -> 160 922.13/297.04 , 1_2(214) -> 213 922.13/297.04 , 1_2(223) -> 222 922.13/297.04 , 1_3(155) -> 61 922.13/297.04 , 1_3(155) -> 66 922.13/297.04 , 1_3(238) -> 96 922.13/297.04 , 2_0(1) -> 1 922.13/297.04 , 2_1(1) -> 43 922.13/297.04 , 2_1(2) -> 1 922.13/297.04 , 2_1(2) -> 6 922.13/297.04 , 2_1(2) -> 43 922.13/297.04 , 2_1(2) -> 75 922.13/297.04 , 2_1(2) -> 97 922.13/297.04 , 2_1(5) -> 4 922.13/297.04 , 2_1(10) -> 9 922.13/297.04 , 2_1(11) -> 40 922.13/297.04 , 2_1(12) -> 7 922.13/297.04 , 2_1(14) -> 8 922.13/297.04 , 2_1(16) -> 12 922.13/297.04 , 2_1(17) -> 12 922.13/297.04 , 2_1(18) -> 12 922.13/297.04 , 2_1(20) -> 80 922.13/297.04 , 2_1(30) -> 26 922.13/297.04 , 2_1(34) -> 43 922.13/297.04 , 2_1(42) -> 76 922.13/297.04 , 2_1(52) -> 51 922.13/297.04 , 2_1(56) -> 7 922.13/297.04 , 2_1(160) -> 43 922.13/297.04 , 2_2(1) -> 97 922.13/297.04 , 2_2(2) -> 97 922.13/297.04 , 2_2(12) -> 97 922.13/297.04 , 2_2(30) -> 97 922.13/297.04 , 2_2(34) -> 97 922.13/297.04 , 2_2(56) -> 12 922.13/297.04 , 2_2(56) -> 43 922.13/297.04 , 2_2(56) -> 97 922.13/297.04 , 2_2(60) -> 59 922.13/297.04 , 2_2(95) -> 94 922.13/297.04 , 2_2(101) -> 100 922.13/297.04 , 2_2(103) -> 98 922.13/297.04 , 2_2(110) -> 103 922.13/297.04 , 2_2(114) -> 113 922.13/297.04 , 2_2(115) -> 114 922.13/297.04 , 2_2(116) -> 222 922.13/297.04 , 2_2(160) -> 43 922.13/297.04 , 2_2(216) -> 215 922.13/297.04 , 2_2(222) -> 213 922.13/297.04 , 3_0(1) -> 1 922.13/297.04 , 3_1(1) -> 11 922.13/297.04 , 3_1(2) -> 11 922.13/297.04 , 3_1(6) -> 5 922.13/297.04 , 3_1(7) -> 11 922.13/297.04 , 3_1(8) -> 11 922.13/297.04 , 3_1(11) -> 10 922.13/297.04 , 3_1(12) -> 1 922.13/297.04 , 3_1(12) -> 11 922.13/297.04 , 3_1(18) -> 55 922.13/297.04 , 3_1(20) -> 19 922.13/297.04 , 3_1(21) -> 11 922.13/297.04 , 3_1(26) -> 11 922.13/297.04 , 3_1(27) -> 11 922.13/297.04 , 3_1(33) -> 32 922.13/297.04 , 3_1(40) -> 39 922.13/297.04 , 3_1(42) -> 9 922.13/297.04 , 3_1(43) -> 42 922.13/297.04 , 3_1(50) -> 49 922.13/297.04 , 3_1(51) -> 11 922.13/297.04 , 3_1(68) -> 1 922.13/297.04 , 3_1(68) -> 11 922.13/297.04 , 3_1(71) -> 70 922.13/297.04 , 3_1(80) -> 51 922.13/297.04 , 3_2(8) -> 60 922.13/297.04 , 3_2(24) -> 23 922.13/297.04 , 3_2(25) -> 224 922.13/297.04 , 3_2(26) -> 102 922.13/297.04 , 3_2(27) -> 60 922.13/297.04 , 3_2(43) -> 217 922.13/297.04 , 3_2(49) -> 217 922.13/297.04 , 3_2(51) -> 102 922.13/297.04 , 3_2(58) -> 57 922.13/297.04 , 3_2(72) -> 11 922.13/297.04 , 3_2(72) -> 55 922.13/297.04 , 3_2(75) -> 74 922.13/297.04 , 3_2(102) -> 101 922.13/297.04 , 3_2(106) -> 105 922.13/297.04 , 3_2(128) -> 126 922.13/297.04 , 3_2(217) -> 216 922.13/297.04 , 3_2(225) -> 224 922.13/297.04 , 3_3(158) -> 157 922.13/297.04 , 3_3(241) -> 240 922.13/297.04 , 5_0(1) -> 1 922.13/297.04 , 5_1(1) -> 33 922.13/297.04 , 5_1(4) -> 3 922.13/297.04 , 5_1(12) -> 2 922.13/297.04 , 5_1(18) -> 3 922.13/297.04 , 5_1(29) -> 28 922.13/297.04 , 5_1(34) -> 1 922.13/297.04 , 5_1(34) -> 18 922.13/297.04 , 5_1(34) -> 111 922.13/297.04 , 5_1(40) -> 50 922.13/297.04 , 5_1(68) -> 2 922.13/297.04 , 5_1(76) -> 50 922.13/297.04 , 5_1(160) -> 1 922.13/297.04 , 5_2(22) -> 21 922.13/297.04 , 5_2(59) -> 58 922.13/297.04 , 5_2(65) -> 64 922.13/297.04 , 5_2(94) -> 93 922.13/297.04 , 5_2(160) -> 1 922.13/297.04 , 5_3(156) -> 155 922.13/297.04 , 5_3(239) -> 238 } 922.13/297.04 922.13/297.04 Hurray, we answered YES(?,O(n^1)) 922.27/297.12 EOF