YES(?,O(n^1))
6.73/1.97	YES(?,O(n^1))
6.73/1.98	
6.73/1.98	Problem:
6.73/1.98	 a(a(a(b(b(x1))))) -> b(b(b(b(b(a(a(a(a(a(x1))))))))))
6.73/1.98	
6.73/1.98	Proof:
6.73/1.98	 Bounds Processor:
6.73/1.98	  bound: 4
6.73/1.98	  enrichment: match
6.73/1.98	  automaton:
6.73/1.98	   final states: {3}
6.73/1.98	   transitions:
6.73/1.98	    a3(262) -> 263*
6.73/1.98	    a3(252) -> 253*
6.73/1.98	    a3(217) -> 218*
6.73/1.98	    a3(177) -> 178*
6.73/1.98	    a3(359) -> 360*
6.73/1.98	    a3(157) -> 158*
6.73/1.98	    a3(334) -> 335*
6.73/1.98	    a3(324) -> 325*
6.73/1.98	    a3(309) -> 310*
6.73/1.98	    a3(299) -> 300*
6.73/1.98	    a3(284) -> 285*
6.73/1.98	    a3(264) -> 265*
6.73/1.98	    a3(249) -> 250*
6.73/1.98	    a3(214) -> 215*
6.73/1.98	    a3(179) -> 180*
6.73/1.98	    a3(356) -> 357*
6.73/1.98	    a3(154) -> 155*
6.73/1.98	    a3(336) -> 337*
6.73/1.98	    a3(321) -> 322*
6.73/1.98	    a3(311) -> 312*
6.73/1.98	    a3(301) -> 302*
6.73/1.98	    a3(286) -> 287*
6.73/1.98	    a3(261) -> 262*
6.73/1.98	    a3(251) -> 252*
6.73/1.98	    a3(216) -> 217*
6.73/1.98	    a3(181) -> 182*
6.73/1.98	    a3(358) -> 359*
6.73/1.98	    a3(156) -> 157*
6.73/1.98	    a3(333) -> 334*
6.73/1.98	    a3(323) -> 324*
6.73/1.98	    a3(308) -> 309*
6.73/1.98	    a3(298) -> 299*
6.73/1.98	    a3(283) -> 284*
6.73/1.98	    a3(263) -> 264*
6.73/1.98	    a3(253) -> 254*
6.73/1.98	    a3(218) -> 219*
6.73/1.98	    a3(178) -> 179*
6.73/1.98	    a3(360) -> 361*
6.73/1.98	    a3(153) -> 154*
6.73/1.98	    a3(335) -> 336*
6.73/1.98	    a3(325) -> 326*
6.73/1.98	    a3(310) -> 311*
6.73/1.98	    a3(300) -> 301*
6.73/1.98	    a3(285) -> 286*
6.73/1.98	    a3(260) -> 261*
6.73/1.98	    a3(250) -> 251*
6.73/1.98	    a3(215) -> 216*
6.73/1.98	    a3(180) -> 181*
6.73/1.98	    a3(357) -> 358*
6.73/1.98	    a3(155) -> 156*
6.73/1.98	    a3(332) -> 333*
6.73/1.98	    a3(322) -> 323*
6.73/1.98	    a3(312) -> 313*
6.73/1.98	    a3(297) -> 298*
6.73/1.98	    a3(282) -> 283*
6.73/1.98	    b4(479) -> 480*
6.73/1.98	    b4(444) -> 445*
6.73/1.98	    b4(434) -> 435*
6.73/1.98	    b4(409) -> 410*
6.73/1.98	    b4(374) -> 375*
6.73/1.98	    b4(349) -> 350*
6.73/1.98	    b4(481) -> 482*
6.73/1.98	    b4(446) -> 447*
6.73/1.98	    b4(431) -> 432*
6.73/1.98	    b4(411) -> 412*
6.73/1.98	    b4(376) -> 377*
6.73/1.98	    b4(351) -> 352*
6.73/1.98	    b4(478) -> 479*
6.73/1.98	    b4(443) -> 444*
6.73/1.98	    b4(433) -> 434*
6.73/1.98	    b4(408) -> 409*
6.73/1.98	    b4(373) -> 374*
6.73/1.98	    b4(348) -> 349*
6.73/1.98	    b4(480) -> 481*
6.73/1.98	    b4(445) -> 446*
6.73/1.98	    b4(435) -> 436*
6.73/1.98	    b4(410) -> 411*
6.73/1.98	    b4(375) -> 376*
6.73/1.98	    b4(350) -> 351*
6.73/1.98	    b4(477) -> 478*
6.73/1.98	    b4(442) -> 443*
6.73/1.98	    b4(432) -> 433*
6.73/1.98	    b4(407) -> 408*
6.73/1.98	    b4(372) -> 373*
6.73/1.98	    b4(352) -> 353*
6.73/1.98	    a4(474) -> 475*
6.73/1.98	    a4(439) -> 440*
6.73/1.98	    a4(429) -> 430*
6.73/1.98	    a4(404) -> 405*
6.73/1.98	    a4(369) -> 370*
6.73/1.98	    a4(344) -> 345*
6.73/1.98	    a4(476) -> 477*
6.73/1.98	    a4(441) -> 442*
6.73/1.98	    a4(426) -> 427*
6.73/1.98	    a4(406) -> 407*
6.73/1.98	    a4(371) -> 372*
6.73/1.98	    a4(346) -> 347*
6.73/1.98	    a4(473) -> 474*
6.73/1.98	    a4(438) -> 439*
6.73/1.98	    a4(428) -> 429*
6.73/1.98	    a4(403) -> 404*
6.73/1.98	    a4(368) -> 369*
6.73/1.98	    a4(343) -> 344*
6.73/1.98	    a4(475) -> 476*
6.73/1.98	    a4(470) -> 471*
6.73/1.98	    a4(440) -> 441*
6.73/1.98	    a4(430) -> 431*
6.73/1.98	    a4(405) -> 406*
6.73/1.98	    a4(400) -> 401*
6.73/1.98	    a4(370) -> 371*
6.73/1.98	    a4(345) -> 346*
6.73/1.98	    a4(472) -> 473*
6.73/1.98	    a4(437) -> 438*
6.73/1.98	    a4(427) -> 428*
6.73/1.98	    a4(402) -> 403*
6.73/1.98	    a4(367) -> 368*
6.73/1.98	    a4(347) -> 348*
6.73/1.98	    a0(3) -> 3*
6.73/1.98	    b0(3) -> 3*
6.73/1.98	    b1(55) -> 56*
6.73/1.98	    b1(20) -> 21*
6.73/1.98	    b1(57) -> 58*
6.73/1.98	    b1(22) -> 23*
6.73/1.98	    b1(59) -> 60*
6.73/1.98	    b1(24) -> 25*
6.73/1.98	    b1(56) -> 57*
6.73/1.98	    b1(21) -> 22*
6.73/1.98	    b1(58) -> 59*
6.73/1.98	    b1(23) -> 24*
6.73/1.98	    a1(50) -> 51*
6.73/1.98	    a1(15) -> 16*
6.73/1.98	    a1(52) -> 53*
6.73/1.98	    a1(17) -> 18*
6.73/1.98	    a1(54) -> 55*
6.73/1.98	    a1(19) -> 20*
6.73/1.98	    a1(76) -> 77*
6.73/1.98	    a1(51) -> 52*
6.73/1.98	    a1(16) -> 17*
6.73/1.98	    a1(78) -> 79*
6.73/1.98	    a1(63) -> 64*
6.73/1.98	    a1(53) -> 54*
6.73/1.98	    a1(18) -> 19*
6.73/1.98	    b2(35) -> 36*
6.73/1.98	    b2(232) -> 233*
6.73/1.98	    b2(172) -> 173*
6.73/1.98	    b2(137) -> 138*
6.73/1.98	    b2(117) -> 118*
6.73/1.98	    b2(234) -> 235*
6.73/1.98	    b2(32) -> 33*
6.73/1.98	    b2(174) -> 175*
6.73/1.98	    b2(134) -> 135*
6.73/1.98	    b2(119) -> 120*
6.73/1.98	    b2(34) -> 35*
6.73/1.98	    b2(231) -> 232*
6.73/1.98	    b2(171) -> 172*
6.73/1.98	    b2(136) -> 137*
6.73/1.98	    b2(121) -> 122*
6.73/1.98	    b2(233) -> 234*
6.73/1.98	    b2(31) -> 32*
6.73/1.98	    b2(173) -> 174*
6.73/1.98	    b2(138) -> 139*
6.73/1.98	    b2(118) -> 119*
6.73/1.98	    b2(33) -> 34*
6.73/1.98	    b2(230) -> 231*
6.73/1.98	    b2(175) -> 176*
6.73/1.98	    b2(135) -> 136*
6.73/1.98	    b2(120) -> 121*
6.73/1.98	    a2(30) -> 31*
6.73/1.98	    a2(227) -> 228*
6.73/1.98	    a2(167) -> 168*
6.73/1.98	    a2(132) -> 133*
6.73/1.98	    a2(127) -> 128*
6.73/1.98	    a2(112) -> 113*
6.73/1.98	    a2(82) -> 83*
6.73/1.98	    a2(229) -> 230*
6.73/1.98	    a2(27) -> 28*
6.73/1.98	    a2(169) -> 170*
6.73/1.98	    a2(129) -> 130*
6.73/1.98	    a2(114) -> 115*
6.73/1.98	    a2(84) -> 85*
6.73/1.98	    a2(29) -> 30*
6.73/1.98	    a2(226) -> 227*
6.73/1.98	    a2(166) -> 167*
6.73/1.98	    a2(151) -> 152*
6.73/1.98	    a2(131) -> 132*
6.73/1.98	    a2(116) -> 117*
6.73/1.98	    a2(228) -> 229*
6.73/1.98	    a2(26) -> 27*
6.73/1.98	    a2(168) -> 169*
6.73/1.98	    a2(133) -> 134*
6.73/1.98	    a2(123) -> 124*
6.73/1.98	    a2(113) -> 114*
6.73/1.98	    a2(28) -> 29*
6.73/1.98	    a2(225) -> 226*
6.73/1.98	    a2(170) -> 171*
6.73/1.98	    a2(130) -> 131*
6.73/1.98	    a2(125) -> 126*
6.73/1.98	    a2(115) -> 116*
6.73/1.98	    b3(267) -> 268*
6.73/1.98	    b3(257) -> 258*
6.73/1.98	    b3(222) -> 223*
6.73/1.98	    b3(182) -> 183*
6.73/1.98	    b3(364) -> 365*
6.73/1.98	    b3(162) -> 163*
6.73/1.98	    b3(339) -> 340*
6.73/1.98	    b3(329) -> 330*
6.73/1.98	    b3(314) -> 315*
6.73/1.98	    b3(304) -> 305*
6.73/1.98	    b3(289) -> 290*
6.73/1.98	    b3(269) -> 270*
6.73/1.98	    b3(254) -> 255*
6.73/1.98	    b3(219) -> 220*
6.73/1.98	    b3(184) -> 185*
6.73/1.98	    b3(361) -> 362*
6.73/1.98	    b3(159) -> 160*
6.73/1.98	    b3(341) -> 342*
6.73/1.98	    b3(326) -> 327*
6.73/1.98	    b3(316) -> 317*
6.73/1.98	    b3(306) -> 307*
6.73/1.98	    b3(291) -> 292*
6.73/1.98	    b3(266) -> 267*
6.73/1.98	    b3(256) -> 257*
6.73/1.98	    b3(221) -> 222*
6.73/1.98	    b3(186) -> 187*
6.73/1.98	    b3(363) -> 364*
6.73/1.98	    b3(161) -> 162*
6.73/1.98	    b3(338) -> 339*
6.73/1.98	    b3(328) -> 329*
6.73/1.98	    b3(313) -> 314*
6.73/1.98	    b3(303) -> 304*
6.73/1.98	    b3(288) -> 289*
6.73/1.98	    b3(268) -> 269*
6.73/1.98	    b3(258) -> 259*
6.73/1.98	    b3(223) -> 224*
6.73/1.98	    b3(183) -> 184*
6.73/1.98	    b3(365) -> 366*
6.73/1.98	    b3(158) -> 159*
6.73/1.98	    b3(340) -> 341*
6.73/1.98	    b3(330) -> 331*
6.73/1.98	    b3(315) -> 316*
6.73/1.98	    b3(305) -> 306*
6.73/1.98	    b3(290) -> 291*
6.73/1.98	    b3(265) -> 266*
6.73/1.98	    b3(255) -> 256*
6.73/1.98	    b3(220) -> 221*
6.73/1.98	    b3(185) -> 186*
6.73/1.98	    b3(362) -> 363*
6.73/1.98	    b3(160) -> 161*
6.73/1.98	    b3(337) -> 338*
6.73/1.98	    b3(327) -> 328*
6.73/1.98	    b3(317) -> 318*
6.73/1.98	    b3(302) -> 303*
6.73/1.98	    b3(287) -> 288*
6.73/1.98	    3 -> 15*
6.73/1.98	    20 -> 129*
6.73/1.98	    21 -> 84*
6.73/1.98	    22 -> 112*
6.73/1.98	    23 -> 63,26
6.73/1.98	    24 -> 50*
6.73/1.98	    25 -> 16,17,18,3
6.73/1.98	    31 -> 214*
6.73/1.98	    32 -> 260*
6.73/1.98	    33 -> 153*
6.73/1.98	    34 -> 177,166
6.73/1.98	    35 -> 125*
6.73/1.98	    36 -> 130,29,20,19,18
6.73/1.98	    55 -> 151*
6.73/1.98	    56 -> 123*
6.73/1.98	    57 -> 127*
6.73/1.98	    58 -> 82,76
6.73/1.98	    59 -> 78*
6.73/1.98	    60 -> 16,17,3,18
6.73/1.98	    64 -> 16*
6.73/1.98	    77 -> 16*
6.73/1.98	    79 -> 16*
6.73/1.98	    83 -> 27*
6.73/1.98	    85 -> 27*
6.73/1.98	    118 -> 297*
6.73/1.98	    120 -> 225*
6.73/1.98	    122 -> 53*
6.73/1.98	    124 -> 27*
6.73/1.98	    126 -> 27*
6.73/1.98	    128 -> 27*
6.73/1.98	    139 -> 115*
6.73/1.98	    152 -> 27*
6.73/1.98	    159 -> 343*
6.73/1.98	    161 -> 321*
6.73/1.98	    163 -> 29*
6.73/1.98	    172 -> 308*
6.73/1.98	    174 -> 249*
6.73/1.98	    176 -> 130,131
6.73/1.98	    183 -> 470*
6.73/1.98	    185 -> 367*
6.73/1.98	    187 -> 215,133,132
6.73/1.98	    224 -> 156*
6.73/1.98	    231 -> 332*
6.73/1.98	    233 -> 282*
6.73/1.98	    235 -> 152*
6.73/1.98	    259 -> 133,134
6.73/1.98	    270 -> 180,169
6.73/1.98	    288 -> 426*
6.73/1.98	    290 -> 356*
6.73/1.98	    292 -> 30*
6.73/1.98	    307 -> 228*
6.73/1.98	    318 -> 252*
6.73/1.98	    327 -> 437*
6.73/1.98	    329 -> 400*
6.73/1.98	    331 -> 215*
6.73/1.98	    342 -> 285*
6.73/1.98	    353 -> 324*
6.73/1.98	    362 -> 472*
6.73/1.98	    364 -> 402*
6.73/1.98	    366 -> 216*
6.73/1.98	    377 -> 218*
6.73/1.98	    401 -> 368*
6.73/1.98	    412 -> 219*
6.73/1.98	    436 -> 359*
6.73/1.98	    447 -> 370*
6.73/1.98	    471 -> 438*
6.73/1.98	    482 -> 405*
6.73/1.98	  problem:
6.73/1.98	   
6.73/1.98	  Qed
6.73/1.98	EOF