YES
by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(x0)))))))))) |
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(0(1(2(x0))))))))))))) |
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))) |
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))) |
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))) |
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))) |
0(1(2(1(x0)))) | → | 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))) |
final states:
{47, 40, 33, 26, 19, 12, 1}
transitions:
33 | → | 5 |
25 | → | 240 |
205 | → | 43 |
32 | → | 244 |
103 | → | 95 |
152 | → | 169 |
97 | → | 102 |
181 | → | 173 |
129 | → | 121 |
149 | → | 154 |
18 | → | 236 |
227 | → | 232 |
39 | → | 248 |
241 | → | 66 |
175 | → | 180 |
1 | → | 5 |
123 | → | 128 |
40 | → | 5 |
71 | → | 76 |
127 | → | 22 |
101 | → | 15 |
179 | → | 36 |
26 | → | 5 |
253 | → | 66 |
233 | → | 225 |
201 | → | 206 |
178 | → | 195 |
207 | → | 199 |
257 | → | 66 |
153 | → | 29 |
75 | → | 8 |
237 | → | 66 |
249 | → | 66 |
204 | → | 221 |
53 | → | 256 |
11 | → | 65 |
12 | → | 5 |
77 | → | 69 |
100 | → | 117 |
126 | → | 143 |
46 | → | 252 |
231 | → | 50 |
245 | → | 66 |
47 | → | 5 |
74 | → | 91 |
19 | → | 5 |
155 | → | 147 |
01(67) | → | 68 |
01(200) | → | 201 |
01(174) | → | 175 |
01(93) | → | 94 |
01(197) | → | 198 |
01(70) | → | 71 |
01(96) | → | 97 |
01(145) | → | 146 |
01(119) | → | 120 |
01(148) | → | 149 |
01(171) | → | 172 |
01(122) | → | 123 |
01(223) | → | 224 |
01(226) | → | 227 |
21(244) | → | 245 |
21(65) | → | 66 |
21(151) | → | 152 |
21(177) | → | 178 |
21(73) | → | 74 |
21(206) | → | 207 |
21(76) | → | 77 |
21(91) | → | 92 |
21(252) | → | 253 |
21(169) | → | 170 |
21(125) | → | 126 |
21(143) | → | 144 |
21(99) | → | 100 |
21(203) | → | 204 |
21(120) | → | 121 |
21(195) | → | 196 |
21(172) | → | 173 |
21(154) | → | 155 |
21(221) | → | 222 |
21(232) | → | 233 |
21(236) | → | 237 |
21(248) | → | 249 |
21(128) | → | 129 |
21(146) | → | 147 |
21(94) | → | 95 |
21(180) | → | 181 |
21(224) | → | 225 |
21(102) | → | 103 |
21(117) | → | 118 |
21(256) | → | 257 |
21(68) | → | 69 |
21(229) | → | 230 |
21(198) | → | 199 |
21(240) | → | 241 |
f30 | → | 2 |
10(20) | → | 21 |
10(51) | → | 52 |
10(37) | → | 38 |
10(29) | → | 30 |
10(43) | → | 44 |
10(9) | → | 10 |
10(8) | → | 9 |
10(32) | → | 26 |
10(41) | → | 42 |
10(15) | → | 16 |
10(18) | → | 12 |
10(16) | → | 17 |
10(27) | → | 28 |
10(25) | → | 19 |
10(23) | → | 24 |
10(6) | → | 7 |
10(39) | → | 33 |
10(36) | → | 37 |
10(30) | → | 31 |
10(11) | → | 1 |
10(44) | → | 45 |
10(46) | → | 40 |
10(50) | → | 51 |
10(3) | → | 4 |
10(13) | → | 14 |
10(48) | → | 49 |
10(22) | → | 23 |
10(34) | → | 35 |
10(53) | → | 47 |
00(28) | → | 29 |
00(14) | → | 15 |
00(7) | → | 8 |
00(49) | → | 50 |
00(4) | → | 5 |
00(42) | → | 43 |
00(35) | → | 36 |
00(21) | → | 22 |
11(149) | → | 150 |
11(196) | → | 197 |
11(123) | → | 124 |
11(227) | → | 228 |
11(204) | → | 205 |
11(230) | → | 231 |
11(175) | → | 176 |
11(202) | → | 203 |
11(98) | → | 99 |
11(95) | → | 96 |
11(170) | → | 171 |
11(225) | → | 226 |
11(152) | → | 153 |
11(71) | → | 72 |
11(92) | → | 93 |
11(124) | → | 125 |
11(222) | → | 223 |
11(74) | → | 75 |
11(150) | → | 151 |
11(178) | → | 179 |
11(147) | → | 148 |
11(176) | → | 177 |
11(100) | → | 101 |
11(118) | → | 119 |
11(66) | → | 67 |
11(121) | → | 122 |
11(173) | → | 174 |
11(228) | → | 229 |
11(201) | → | 202 |
11(126) | → | 127 |
11(97) | → | 98 |
11(144) | → | 145 |
11(199) | → | 200 |
11(72) | → | 73 |
11(69) | → | 70 |
20(22) | → | 27 |
20(38) | → | 39 |
20(24) | → | 25 |
20(8) | → | 13 |
20(10) | → | 11 |
20(15) | → | 20 |
20(29) | → | 34 |
20(17) | → | 18 |
20(45) | → | 46 |
20(5) | → | 6 |
20(31) | → | 32 |
20(2) | → | 3 |
20(52) | → | 53 |
20(36) | → | 41 |
20(43) | → | 48 |