YES(?,O(n^1)) Problem: a(a(a(b(b(b(x1)))))) -> b(b(b(b(a(a(a(a(x1)))))))) Proof: Bounds Processor: bound: 5 enrichment: match automaton: final states: {3} transitions: a3(202) -> 203* a3(182) -> 183* a3(142) -> 143* a3(199) -> 200* a3(189) -> 190* a3(179) -> 180* a3(139) -> 140* a3(201) -> 202* a3(191) -> 192* a3(181) -> 182* a3(166) -> 167* a3(141) -> 142* a3(188) -> 189* a3(200) -> 201* a3(190) -> 191* a3(180) -> 181* a3(140) -> 141* b4(232) -> 233* b4(249) -> 250* b4(251) -> 252* b4(231) -> 232* b4(248) -> 249* b4(233) -> 234* b4(250) -> 251* b4(230) -> 231* a4(247) -> 248* a4(227) -> 228* a4(244) -> 245* a4(229) -> 230* a4(246) -> 247* a4(226) -> 227* a4(228) -> 229* a4(245) -> 246* a0(3) -> 3* b5(257) -> 258* b5(259) -> 260* b5(258) -> 259* b5(260) -> 261* b0(3) -> 3* a5(254) -> 255* a5(256) -> 257* a5(253) -> 254* a5(255) -> 256* b1(20) -> 21* b1(27) -> 28* b1(17) -> 18* b1(29) -> 30* b1(19) -> 20* b1(26) -> 27* b1(28) -> 29* b1(18) -> 19* a1(25) -> 26* a1(15) -> 16* a1(42) -> 43* a1(22) -> 23* a1(44) -> 45* a1(24) -> 25* a1(14) -> 15* a1(91) -> 92* a1(16) -> 17* a1(83) -> 84* a1(23) -> 24* a1(13) -> 14* a1(85) -> 86* b2(75) -> 76* b2(65) -> 66* b2(152) -> 153* b2(97) -> 98* b2(72) -> 73* b2(154) -> 155* b2(99) -> 100* b2(74) -> 75* b2(64) -> 65* b2(66) -> 67* b2(153) -> 154* b2(98) -> 99* b2(73) -> 74* b2(63) -> 64* b2(155) -> 156* b2(100) -> 101* a2(70) -> 71* a2(60) -> 61* a2(77) -> 78* a2(62) -> 63* a2(149) -> 150* a2(129) -> 130* a2(94) -> 95* a2(69) -> 70* a2(59) -> 60* a2(151) -> 152* a2(131) -> 132* a2(96) -> 97* a2(71) -> 72* a2(61) -> 62* a2(148) -> 149* a2(93) -> 94* a2(68) -> 69* a2(150) -> 151* a2(135) -> 136* a2(95) -> 96* b3(192) -> 193* b3(204) -> 205* b3(194) -> 195* b3(184) -> 185* b3(144) -> 145* b3(206) -> 207* b3(186) -> 187* b3(146) -> 147* b3(203) -> 204* b3(193) -> 194* b3(183) -> 184* b3(143) -> 144* b3(205) -> 206* b3(195) -> 196* b3(185) -> 186* b3(145) -> 146* 3 -> 13* 17 -> 68* 18 -> 59,22 19 -> 42* 20 -> 44* 21 -> 16,14,15,3 26 -> 135* 27 -> 83,77 28 -> 85* 29 -> 91* 30 -> 16,14,3,15 43 -> 23* 45 -> 23* 63 -> 166* 64 -> 139,93 65 -> 131* 66 -> 129* 67 -> 69,70,17,16 73 -> 199,148 76 -> 62,25 78 -> 60* 84 -> 14* 86 -> 14* 92 -> 14* 101 -> 70* 130 -> 69* 132 -> 69* 136 -> 60* 145 -> 188* 147 -> 72,71 153 -> 179* 156 -> 61* 167 -> 140* 184 -> 226* 187 -> 167,140 196 -> 202,151 207 -> 141* 230 -> 253* 233 -> 244* 234 -> 143* 252 -> 191* 261 -> 247* problem: Qed