YES(?,O(n^1)) 0.15/0.52 YES(?,O(n^1)) 0.15/0.52 0.15/0.52 Problem: 0.15/0.52 b(c(b(c(a(a(x1)))))) -> a(a(a(b(c(b(c(b(c(x1))))))))) 0.15/0.52 0.15/0.52 Proof: 0.15/0.52 Bounds Processor: 0.15/0.52 bound: 5 0.15/0.52 enrichment: match 0.15/0.52 automaton: 0.15/0.52 final states: {4} 0.15/0.52 transitions: 0.15/0.52 b3(242) -> 243* 0.15/0.52 b3(314) -> 315* 0.15/0.52 b3(164) -> 165* 0.15/0.52 b3(154) -> 155* 0.15/0.52 b3(206) -> 207* 0.15/0.52 b3(196) -> 197* 0.15/0.52 b3(166) -> 167* 0.15/0.52 b3(156) -> 157* 0.15/0.52 b3(106) -> 107* 0.15/0.52 b3(238) -> 239* 0.15/0.52 b3(208) -> 209* 0.15/0.52 b3(198) -> 199* 0.15/0.52 b3(168) -> 169* 0.15/0.52 b3(158) -> 159* 0.15/0.52 b3(310) -> 311* 0.15/0.52 b3(108) -> 109* 0.15/0.52 b3(240) -> 241* 0.15/0.52 b3(210) -> 211* 0.15/0.52 b3(200) -> 201* 0.15/0.52 b3(312) -> 313* 0.15/0.52 b3(110) -> 111* 0.15/0.52 c3(237) -> 238* 0.15/0.52 c3(207) -> 208* 0.15/0.52 c3(197) -> 198* 0.15/0.52 c3(167) -> 168* 0.15/0.52 c3(157) -> 158* 0.15/0.52 c3(309) -> 310* 0.15/0.52 c3(107) -> 108* 0.15/0.52 c3(239) -> 240* 0.15/0.52 c3(209) -> 210* 0.15/0.52 c3(199) -> 200* 0.15/0.52 c3(311) -> 312* 0.15/0.52 c3(109) -> 110* 0.15/0.52 c3(241) -> 242* 0.15/0.52 c3(313) -> 314* 0.15/0.52 c3(163) -> 164* 0.15/0.52 c3(153) -> 154* 0.15/0.52 c3(235) -> 236* 0.15/0.52 c3(205) -> 206* 0.15/0.52 c3(195) -> 196* 0.15/0.52 c3(165) -> 166* 0.15/0.52 c3(155) -> 156* 0.15/0.52 c3(105) -> 106* 0.15/0.52 a4(399) -> 400* 0.15/0.52 a4(369) -> 370* 0.15/0.52 a4(359) -> 360* 0.15/0.52 a4(284) -> 285* 0.15/0.52 a4(264) -> 265* 0.15/0.52 a4(401) -> 402* 0.15/0.52 a4(371) -> 372* 0.15/0.52 a4(361) -> 362* 0.15/0.52 a4(336) -> 337* 0.15/0.52 a4(283) -> 284* 0.15/0.52 a4(263) -> 264* 0.15/0.52 a4(400) -> 401* 0.15/0.52 a4(370) -> 371* 0.15/0.52 a4(360) -> 361* 0.15/0.52 a4(335) -> 336* 0.15/0.52 a4(285) -> 286* 0.15/0.52 a4(265) -> 266* 0.15/0.52 a4(337) -> 338* 0.15/0.52 b4(282) -> 283* 0.15/0.52 b4(262) -> 263* 0.15/0.52 b4(394) -> 395* 0.15/0.52 b4(364) -> 365* 0.15/0.52 b4(354) -> 355* 0.15/0.52 b4(334) -> 335* 0.15/0.52 b4(396) -> 397* 0.15/0.52 b4(366) -> 367* 0.15/0.52 b4(356) -> 357* 0.15/0.52 b4(398) -> 399* 0.15/0.52 b4(368) -> 369* 0.15/0.52 b4(358) -> 359* 0.15/0.52 b4(278) -> 279* 0.15/0.52 b4(258) -> 259* 0.15/0.52 b4(330) -> 331* 0.15/0.52 b4(280) -> 281* 0.15/0.52 b4(260) -> 261* 0.15/0.52 b4(332) -> 333* 0.15/0.52 b0(4) -> 4* 0.15/0.52 c4(277) -> 278* 0.15/0.52 c4(257) -> 258* 0.15/0.52 c4(339) -> 340* 0.15/0.52 c4(329) -> 330* 0.15/0.52 c4(279) -> 280* 0.15/0.52 c4(259) -> 260* 0.15/0.52 c4(331) -> 332* 0.15/0.52 c4(281) -> 282* 0.15/0.52 c4(261) -> 262* 0.15/0.52 c4(393) -> 394* 0.15/0.52 c4(363) -> 364* 0.15/0.52 c4(353) -> 354* 0.15/0.52 c4(333) -> 334* 0.15/0.52 c4(395) -> 396* 0.15/0.52 c4(365) -> 366* 0.15/0.52 c4(355) -> 356* 0.15/0.52 c4(397) -> 398* 0.15/0.52 c4(367) -> 368* 0.15/0.52 c4(357) -> 358* 0.15/0.52 c4(287) -> 288* 0.15/0.52 c0(4) -> 4* 0.15/0.52 a5(439) -> 440* 0.15/0.52 a5(409) -> 410* 0.15/0.52 a5(441) -> 442* 0.15/0.52 a5(411) -> 412* 0.15/0.52 a5(440) -> 441* 0.15/0.52 a5(410) -> 411* 0.15/0.52 a0(4) -> 4* 0.15/0.52 b5(434) -> 435* 0.15/0.52 b5(404) -> 405* 0.15/0.52 b5(436) -> 437* 0.15/0.52 b5(406) -> 407* 0.15/0.52 b5(438) -> 439* 0.15/0.52 b5(408) -> 409* 0.15/0.52 a1(45) -> 46* 0.15/0.52 a1(47) -> 48* 0.15/0.52 a1(22) -> 23* 0.15/0.52 a1(46) -> 47* 0.15/0.52 a1(21) -> 22* 0.15/0.52 a1(23) -> 24* 0.15/0.52 c5(433) -> 434* 0.15/0.52 c5(403) -> 404* 0.15/0.52 c5(435) -> 436* 0.15/0.52 c5(405) -> 406* 0.15/0.52 c5(437) -> 438* 0.15/0.52 c5(407) -> 408* 0.15/0.52 b1(40) -> 41* 0.15/0.52 b1(20) -> 21* 0.15/0.52 b1(42) -> 43* 0.15/0.52 b1(44) -> 45* 0.15/0.52 b1(16) -> 17* 0.15/0.52 b1(18) -> 19* 0.15/0.52 c1(15) -> 16* 0.15/0.52 c1(17) -> 18* 0.15/0.52 c1(99) -> 100* 0.15/0.52 c1(69) -> 70* 0.15/0.52 c1(39) -> 40* 0.15/0.52 c1(19) -> 20* 0.15/0.52 c1(41) -> 42* 0.15/0.52 c1(43) -> 44* 0.15/0.52 c1(85) -> 86* 0.15/0.52 a2(137) -> 138* 0.15/0.52 a2(32) -> 33* 0.15/0.52 a2(179) -> 180* 0.15/0.52 a2(139) -> 140* 0.15/0.52 a2(79) -> 80* 0.15/0.52 a2(181) -> 182* 0.15/0.52 a2(81) -> 82* 0.15/0.52 a2(31) -> 32* 0.15/0.52 a2(138) -> 139* 0.15/0.52 a2(33) -> 34* 0.15/0.52 a2(180) -> 181* 0.15/0.52 a2(80) -> 81* 0.15/0.52 b2(30) -> 31* 0.15/0.52 b2(132) -> 133* 0.15/0.52 b2(174) -> 175* 0.15/0.52 b2(134) -> 135* 0.15/0.52 b2(74) -> 75* 0.15/0.52 b2(176) -> 177* 0.15/0.52 b2(136) -> 137* 0.15/0.52 b2(76) -> 77* 0.15/0.52 b2(26) -> 27* 0.15/0.52 b2(178) -> 179* 0.15/0.52 b2(78) -> 79* 0.15/0.52 b2(28) -> 29* 0.15/0.52 c2(75) -> 76* 0.15/0.52 c2(25) -> 26* 0.15/0.52 c2(177) -> 178* 0.15/0.52 c2(127) -> 128* 0.15/0.52 c2(77) -> 78* 0.15/0.52 c2(27) -> 28* 0.15/0.52 c2(29) -> 30* 0.15/0.52 c2(131) -> 132* 0.15/0.52 c2(173) -> 174* 0.15/0.52 c2(133) -> 134* 0.15/0.52 c2(83) -> 84* 0.15/0.52 c2(73) -> 74* 0.15/0.52 c2(175) -> 176* 0.15/0.52 c2(135) -> 136* 0.15/0.52 c2(115) -> 116* 0.15/0.52 a3(212) -> 213* 0.15/0.52 a3(202) -> 203* 0.15/0.52 a3(112) -> 113* 0.15/0.52 a3(244) -> 245* 0.15/0.52 a3(169) -> 170* 0.15/0.52 a3(159) -> 160* 0.15/0.52 a3(316) -> 317* 0.15/0.52 a3(211) -> 212* 0.15/0.52 a3(201) -> 202* 0.15/0.52 a3(171) -> 172* 0.15/0.52 a3(161) -> 162* 0.15/0.52 a3(111) -> 112* 0.15/0.52 a3(243) -> 244* 0.15/0.52 a3(213) -> 214* 0.15/0.52 a3(203) -> 204* 0.15/0.52 a3(315) -> 316* 0.15/0.52 a3(113) -> 114* 0.15/0.52 a3(245) -> 246* 0.15/0.52 a3(170) -> 171* 0.15/0.52 a3(160) -> 161* 0.15/0.52 a3(317) -> 318* 0.15/0.52 4 -> 15* 0.15/0.52 21 -> 73* 0.15/0.52 22 -> 69,25 0.15/0.52 23 -> 39* 0.15/0.52 24 -> 17,19,4 0.15/0.52 31 -> 163* 0.15/0.52 32 -> 131,105 0.15/0.52 33 -> 115* 0.15/0.52 34 -> 75,29,21,19 0.15/0.52 45 -> 127* 0.15/0.52 46 -> 99,83 0.15/0.52 47 -> 85* 0.15/0.52 48 -> 17,4,15,19 0.15/0.52 70 -> 16* 0.15/0.52 80 -> 173* 0.15/0.52 82 -> 43* 0.15/0.52 84 -> 26* 0.15/0.52 86 -> 16* 0.15/0.52 100 -> 16* 0.15/0.52 111 -> 329* 0.15/0.52 112 -> 277* 0.15/0.52 113 -> 235* 0.15/0.52 114 -> 165,79,77 0.15/0.52 116 -> 26* 0.15/0.52 128 -> 26* 0.15/0.52 138 -> 153* 0.15/0.52 140 -> 75* 0.15/0.52 159 -> 339* 0.15/0.52 161 -> 205* 0.15/0.52 162 -> 79* 0.15/0.52 170 -> 237* 0.15/0.52 172 -> 29* 0.15/0.52 180 -> 195* 0.15/0.52 182 -> 27* 0.15/0.52 201 -> 353* 0.15/0.52 202 -> 257* 0.15/0.52 203 -> 309* 0.15/0.52 204 -> 31* 0.15/0.52 214 -> 177* 0.15/0.52 236 -> 206* 0.15/0.52 244 -> 287* 0.15/0.52 246 -> 165* 0.15/0.52 266 -> 167* 0.15/0.52 283 -> 403* 0.15/0.52 285 -> 363* 0.15/0.52 286 -> 169* 0.15/0.52 288 -> 278* 0.15/0.52 316 -> 393* 0.15/0.52 318 -> 109,135 0.15/0.52 338 -> 209* 0.15/0.52 340 -> 330* 0.15/0.52 362 -> 313* 0.15/0.52 372 -> 241* 0.15/0.52 400 -> 433* 0.15/0.52 402 -> 331* 0.15/0.52 412 -> 367* 0.15/0.52 442 -> 335* 0.15/0.52 problem: 0.15/0.52 0.15/0.52 Qed 0.15/0.53 EOF