YES(?,O(n^1)) 6.70/1.94 YES(?,O(n^1)) 6.70/1.95 6.70/1.95 Problem: 6.70/1.95 t(o(x1)) -> m(a(x1)) 6.70/1.95 t(e(x1)) -> n(s(x1)) 6.70/1.95 a(l(x1)) -> a(t(x1)) 6.70/1.95 o(m(a(x1))) -> t(e(n(x1))) 6.70/1.95 s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) 6.70/1.95 n(s(x1)) -> a(l(a(t(x1)))) 6.70/1.95 6.70/1.95 Proof: 6.70/1.95 Bounds Processor: 6.70/1.95 bound: 8 6.70/1.95 enrichment: match 6.70/1.95 automaton: 6.70/1.95 final states: {9} 6.70/1.95 transitions: 6.70/1.95 l3(299) -> 300* 6.70/1.95 l3(234) -> 235* 6.70/1.95 l3(229) -> 230* 6.70/1.95 l3(204) -> 205* 6.70/1.95 t3(297) -> 298* 6.70/1.95 t3(232) -> 233* 6.70/1.95 t3(227) -> 228* 6.70/1.95 t3(202) -> 203* 6.70/1.95 t3(528) -> 529* 6.70/1.95 t3(580) -> 581* 6.70/1.95 t3(293) -> 294* 6.70/1.95 t3(198) -> 199* 6.70/1.95 t3(163) -> 164* 6.70/1.95 t3(360) -> 361* 6.70/1.95 t3(447) -> 448* 6.70/1.95 t3(195) -> 196* 6.70/1.95 t3(534) -> 535* 6.70/1.95 o3(296) -> 297* 6.70/1.95 o3(201) -> 202* 6.70/1.95 m3(134) -> 135* 6.70/1.95 m3(295) -> 296* 6.70/1.95 m3(200) -> 201* 6.70/1.95 e3(292) -> 293* 6.70/1.95 e3(429) -> 430* 6.70/1.95 e3(197) -> 198* 6.70/1.95 e3(314) -> 315* 6.70/1.95 e3(194) -> 195* 6.70/1.95 n3(161) -> 162* 6.70/1.95 n3(141) -> 142* 6.70/1.95 n3(193) -> 194* 6.70/1.95 s3(476) -> 477* 6.70/1.95 s3(254) -> 255* 6.70/1.95 s3(381) -> 382* 6.70/1.95 s3(383) -> 384* 6.70/1.95 s3(160) -> 161* 6.70/1.95 s3(140) -> 141* 6.70/1.95 a4(237) -> 238* 6.70/1.95 a4(354) -> 355* 6.70/1.95 a4(349) -> 350* 6.70/1.95 a4(366) -> 367* 6.70/1.95 a4(336) -> 337* 6.70/1.95 a4(263) -> 264* 6.70/1.95 a4(270) -> 271* 6.70/1.95 a4(352) -> 353* 6.70/1.95 a4(347) -> 348* 6.70/1.95 a4(332) -> 333* 6.70/1.95 l4(353) -> 354* 6.70/1.95 l4(348) -> 349* 6.70/1.95 l4(337) -> 338* 6.70/1.95 t0(9) -> 9* 6.70/1.95 t4(262) -> 263* 6.70/1.95 t4(526) -> 527* 6.70/1.95 t4(269) -> 270* 6.70/1.95 t4(578) -> 579* 6.70/1.95 t4(351) -> 352* 6.70/1.95 t4(346) -> 347* 6.70/1.95 t4(331) -> 332* 6.70/1.95 t4(286) -> 287* 6.70/1.95 t4(418) -> 419* 6.70/1.95 t4(520) -> 521* 6.70/1.95 t4(445) -> 446* 6.70/1.95 t4(335) -> 336* 6.70/1.95 o0(9) -> 9* 6.70/1.95 o4(334) -> 335* 6.70/1.95 m0(9) -> 9* 6.70/1.95 m4(333) -> 334* 6.70/1.95 m4(238) -> 239* 6.70/1.95 m4(367) -> 368* 6.70/1.95 a0(9) -> 9* 6.70/1.95 e4(330) -> 331* 6.70/1.95 e4(285) -> 286* 6.70/1.95 e4(417) -> 418* 6.70/1.95 e0(9) -> 9* 6.70/1.95 n4(252) -> 253* 6.70/1.95 n4(284) -> 285* 6.70/1.95 n4(244) -> 245* 6.70/1.95 n4(416) -> 417* 6.70/1.95 n4(390) -> 391* 6.70/1.95 n0(9) -> 9* 6.70/1.95 s4(389) -> 390* 6.70/1.95 s4(379) -> 380* 6.70/1.95 s4(251) -> 252* 6.70/1.95 s4(465) -> 466* 6.70/1.95 s4(243) -> 244* 6.70/1.95 s0(9) -> 9* 6.70/1.95 a5(399) -> 400* 6.70/1.95 a5(516) -> 517* 6.70/1.95 a5(441) -> 442* 6.70/1.95 a5(436) -> 437* 6.70/1.95 a5(518) -> 519* 6.70/1.95 a5(443) -> 444* 6.70/1.95 a5(438) -> 439* 6.70/1.95 a5(373) -> 374* 6.70/1.95 a5(405) -> 406* 6.70/1.95 l0(9) -> 9* 6.70/1.95 l5(517) -> 518* 6.70/1.95 l5(442) -> 443* 6.70/1.95 l5(437) -> 438* 6.70/1.95 a1(40) -> 41* 6.70/1.95 a1(24) -> 25* 6.70/1.95 a1(36) -> 37* 6.70/1.95 a1(13) -> 14* 6.70/1.95 t5(404) -> 405* 6.70/1.95 t5(506) -> 507* 6.70/1.95 t5(398) -> 399* 6.70/1.95 t5(515) -> 516* 6.70/1.95 t5(440) -> 441* 6.70/1.95 t5(435) -> 436* 6.70/1.95 t5(572) -> 573* 6.70/1.95 t5(427) -> 428* 6.70/1.95 l1(41) -> 42* 6.70/1.95 l1(43) -> 44* 6.70/1.95 e5(426) -> 427* 6.70/1.95 t1(35) -> 36* 6.70/1.95 t1(74) -> 75* 6.70/1.95 t1(39) -> 40* 6.70/1.95 t1(28) -> 29* 6.70/1.95 t1(23) -> 24* 6.70/1.95 n5(396) -> 397* 6.70/1.95 n5(463) -> 464* 6.70/1.95 n5(425) -> 426* 6.70/1.95 n5(377) -> 378* 6.70/1.95 o1(38) -> 39* 6.70/1.95 s5(376) -> 377* 6.70/1.95 s5(395) -> 396* 6.70/1.95 s5(462) -> 463* 6.70/1.95 m1(37) -> 38* 6.70/1.95 m1(14) -> 15* 6.70/1.95 m5(374) -> 375* 6.70/1.95 e1(431) -> 432* 6.70/1.95 e1(27) -> 28* 6.70/1.95 e1(214) -> 215* 6.70/1.95 e1(316) -> 317* 6.70/1.95 e1(104) -> 105* 6.70/1.95 e1(34) -> 35* 6.70/1.95 e1(322) -> 323* 6.70/1.95 a6(504) -> 505* 6.70/1.95 a6(499) -> 500* 6.70/1.95 a6(568) -> 569* 6.70/1.95 a6(483) -> 484* 6.70/1.95 a6(570) -> 571* 6.70/1.95 a6(490) -> 491* 6.70/1.95 a6(552) -> 553* 6.70/1.95 a6(502) -> 503* 6.70/1.95 a6(497) -> 498* 6.70/1.95 n1(282) -> 283* 6.70/1.95 n1(17) -> 18* 6.70/1.95 n1(94) -> 95* 6.70/1.95 n1(276) -> 277* 6.70/1.95 n1(186) -> 187* 6.70/1.95 n1(26) -> 27* 6.70/1.95 n1(420) -> 421* 6.70/1.95 n1(188) -> 189* 6.70/1.95 n1(88) -> 89* 6.70/1.95 l6(503) -> 504* 6.70/1.95 l6(498) -> 499* 6.70/1.95 l6(569) -> 570* 6.70/1.95 s1(16) -> 17* 6.70/1.95 t6(489) -> 490* 6.70/1.95 t6(551) -> 552* 6.70/1.95 t6(501) -> 502* 6.70/1.95 t6(496) -> 497* 6.70/1.95 t6(567) -> 568* 6.70/1.95 t6(482) -> 483* 6.70/1.95 a2(112) -> 113* 6.70/1.95 a2(49) -> 50* 6.70/1.95 a2(81) -> 82* 6.70/1.95 a2(108) -> 109* 6.70/1.95 a2(68) -> 69* 6.70/1.95 a2(120) -> 121* 6.70/1.95 n6(454) -> 455* 6.70/1.95 l2(121) -> 122* 6.70/1.95 l2(113) -> 114* 6.70/1.95 s6(453) -> 454* 6.70/1.95 t2(80) -> 81* 6.70/1.95 t2(107) -> 108* 6.70/1.95 t2(67) -> 68* 6.70/1.95 t2(119) -> 120* 6.70/1.95 t2(111) -> 112* 6.70/1.95 t2(98) -> 99* 6.70/1.95 a7(541) -> 542* 6.70/1.95 a7(593) -> 594* 6.70/1.95 a7(558) -> 559* 6.70/1.95 a7(560) -> 561* 6.70/1.95 a7(549) -> 550* 6.70/1.95 o2(110) -> 111* 6.70/1.95 l7(559) -> 560* 6.70/1.95 m2(50) -> 51* 6.70/1.95 m2(109) -> 110* 6.70/1.95 t7(548) -> 549* 6.70/1.95 t7(540) -> 541* 6.70/1.95 t7(592) -> 593* 6.70/1.95 t7(557) -> 558* 6.70/1.95 e2(324) -> 325* 6.70/1.95 e2(97) -> 98* 6.70/1.95 e2(433) -> 434* 6.70/1.95 e2(216) -> 217* 6.70/1.95 e2(328) -> 329* 6.70/1.95 e2(106) -> 107* 6.70/1.95 a8(588) -> 589* 6.70/1.95 n2(65) -> 66* 6.70/1.95 n2(96) -> 97* 6.70/1.95 n2(58) -> 59* 6.70/1.95 t8(587) -> 588* 6.70/1.95 s2(147) -> 148* 6.70/1.95 s2(57) -> 58* 6.70/1.95 s2(478) -> 479* 6.70/1.95 s2(64) -> 65* 6.70/1.95 s2(256) -> 257* 6.70/1.95 s2(385) -> 386* 6.70/1.95 s2(387) -> 388* 6.70/1.95 a3(294) -> 295* 6.70/1.95 a3(199) -> 200* 6.70/1.95 a3(164) -> 165* 6.70/1.95 a3(298) -> 299* 6.70/1.95 a3(233) -> 234* 6.70/1.95 a3(228) -> 229* 6.70/1.95 a3(203) -> 204* 6.70/1.95 a3(133) -> 134* 6.70/1.95 a3(235) -> 236* 6.70/1.95 a3(230) -> 231* 6.70/1.95 9 -> 34,26,23,16,13 6.70/1.95 13 -> 88* 6.70/1.95 15 -> 228,120,24,9 6.70/1.95 16 -> 119* 6.70/1.95 18 -> 228,120,24,9 6.70/1.95 24 -> 106,104,94 6.70/1.95 25 -> 89,27,14,43,9 6.70/1.95 27 -> 57* 6.70/1.95 29 -> 9* 6.70/1.95 34 -> 64* 6.70/1.95 36 -> 96* 6.70/1.95 38 -> 49* 6.70/1.95 41 -> 80,74 6.70/1.95 42 -> 65,17,9 6.70/1.95 43 -> 67* 6.70/1.95 44 -> 24* 6.70/1.95 51 -> 40* 6.70/1.95 57 -> 232* 6.70/1.95 59 -> 29* 6.70/1.95 64 -> 227* 6.70/1.95 66 -> 36* 6.70/1.95 68 -> 216,214,197,188 6.70/1.95 69 -> 18,25,9,43 6.70/1.95 75 -> 24* 6.70/1.95 81 -> 186* 6.70/1.95 82 -> 14* 6.70/1.95 89 -> 27* 6.70/1.95 95 -> 27* 6.70/1.95 97 -> 140* 6.70/1.95 99 -> 39* 6.70/1.95 104 -> 147* 6.70/1.95 105 -> 35* 6.70/1.96 106 -> 160* 6.70/1.96 108 -> 193* 6.70/1.96 110 -> 133* 6.70/1.96 114 -> 58,65,17 6.70/1.96 121 -> 163* 6.70/1.96 122 -> 68* 6.70/1.96 135 -> 112* 6.70/1.96 140 -> 351* 6.70/1.96 142 -> 99,39 6.70/1.96 147 -> 360* 6.70/1.96 148 -> 65* 6.70/1.96 160 -> 346* 6.70/1.96 162 -> 108* 6.70/1.96 164 -> 330,324,316,292,276 6.70/1.96 165 -> 69,25,43,14,27,67,18,94,106 6.70/1.96 187 -> 27* 6.70/1.96 189 -> 27* 6.70/1.96 194 -> 251* 6.70/1.96 196 -> 111* 6.70/1.96 197 -> 243* 6.70/1.96 199 -> 284* 6.70/1.96 201 -> 237* 6.70/1.96 205 -> 161,148,58,65 6.70/1.96 214 -> 256* 6.70/1.96 215 -> 35* 6.70/1.96 216 -> 254* 6.70/1.96 217 -> 107* 6.70/1.96 229 -> 269* 6.70/1.96 231 -> 66,36,96 6.70/1.96 234 -> 262* 6.70/1.96 235 -> 328,322,314,282 6.70/1.96 236 -> 59* 6.70/1.96 239 -> 203* 6.70/1.96 243 -> 440* 6.70/1.96 245 -> 199* 6.70/1.96 251 -> 435* 6.70/1.96 253 -> 196,111 6.70/1.96 254 -> 445* 6.70/1.96 255 -> 161* 6.70/1.96 256 -> 447* 6.70/1.96 257 -> 65* 6.70/1.96 263 -> 433,431,429,420 6.70/1.96 264 -> 236,59,29 6.70/1.96 271 -> 231* 6.70/1.96 277 -> 27* 6.70/1.96 283 -> 27* 6.70/1.96 285 -> 376* 6.70/1.96 287 -> 202* 6.70/1.96 292 -> 389* 6.70/1.96 294 -> 416* 6.70/1.96 296 -> 366* 6.70/1.96 300 -> 58,148 6.70/1.96 314 -> 379* 6.70/1.96 315 -> 198* 6.70/1.96 316 -> 385* 6.70/1.96 317 -> 35* 6.70/1.96 322 -> 387* 6.70/1.96 323 -> 35* 6.70/1.96 324 -> 381* 6.70/1.96 325 -> 107* 6.70/1.96 328 -> 383* 6.70/1.96 329 -> 107* 6.70/1.96 330 -> 395* 6.70/1.96 332 -> 425* 6.70/1.96 334 -> 373* 6.70/1.96 338 -> 161* 6.70/1.96 348 -> 404* 6.70/1.96 350 -> 162,108,193 6.70/1.96 353 -> 398* 6.70/1.96 355 -> 142* 6.70/1.96 361 -> 228* 6.70/1.96 368 -> 298* 6.70/1.96 375 -> 336* 6.70/1.96 376 -> 501* 6.70/1.96 378 -> 287* 6.70/1.96 379 -> 506* 6.70/1.96 380 -> 244* 6.70/1.96 381 -> 520* 6.70/1.96 382 -> 161* 6.70/1.96 383 -> 526* 6.70/1.96 384 -> 161* 6.70/1.96 385 -> 528* 6.70/1.96 386 -> 65* 6.70/1.96 387 -> 534* 6.70/1.96 388 -> 65* 6.70/1.96 389 -> 515* 6.70/1.96 391 -> 294* 6.70/1.96 395 -> 496* 6.70/1.96 397 -> 332* 6.70/1.96 400 -> 355,142,99 6.70/1.96 406 -> 350,162 6.70/1.96 417 -> 462* 6.70/1.96 419 -> 297* 6.70/1.96 421 -> 27* 6.70/1.96 426 -> 453* 6.70/1.96 428 -> 335* 6.70/1.96 429 -> 465* 6.70/1.96 430 -> 198* 6.70/1.96 431 -> 478* 6.70/1.96 432 -> 35* 6.70/1.96 433 -> 476* 6.70/1.96 434 -> 107* 6.70/1.96 437 -> 489* 6.70/1.96 439 -> 253,196 6.70/1.96 442 -> 482* 6.70/1.96 444 -> 245* 6.70/1.96 446 -> 347* 6.70/1.96 448 -> 228* 6.70/1.96 453 -> 557* 6.70/1.96 455 -> 428,335 6.70/1.96 462 -> 567* 6.70/1.96 464 -> 419,297 6.70/1.96 465 -> 572* 6.70/1.96 466 -> 244* 6.70/1.96 476 -> 578* 6.70/1.96 477 -> 161* 6.70/1.96 478 -> 580* 6.70/1.96 479 -> 65* 6.70/1.96 484 -> 444,245,284 6.70/1.96 491 -> 439,253,196,111 6.70/1.96 498 -> 548* 6.70/1.96 500 -> 397,332,425 6.70/1.96 503 -> 540* 6.70/1.96 505 -> 378* 6.70/1.96 507 -> 441* 6.70/1.96 517 -> 551* 6.70/1.96 519 -> 391* 6.70/1.96 521 -> 347* 6.70/1.96 527 -> 347* 6.70/1.96 529 -> 228* 6.70/1.96 535 -> 228* 6.70/1.96 542 -> 505,378,202 6.70/1.96 550 -> 500,397 6.70/1.96 553 -> 519,391,416 6.70/1.96 559 -> 587* 6.70/1.96 561 -> 455,428 6.70/1.96 569 -> 592* 6.70/1.96 571 -> 464* 6.70/1.96 573 -> 441* 6.70/1.96 579 -> 347* 6.70/1.96 581 -> 228* 6.70/1.96 589 -> 561,455,428,335 6.70/1.96 594 -> 571,464,419 6.70/1.96 problem: 6.70/1.96 6.70/1.96 Qed 6.70/1.96 EOF