YES Problem: 2(5(3(0(x1)))) -> 1(0(0(1(3(0(4(5(1(2(x1)))))))))) 1(3(5(4(3(x1))))) -> 2(1(4(1(4(0(3(0(1(1(x1)))))))))) 5(1(3(5(0(x1))))) -> 5(1(4(3(0(4(4(5(2(1(x1)))))))))) 5(4(4(2(5(x1))))) -> 4(3(1(1(1(1(5(3(3(5(x1)))))))))) 2(2(5(0(5(4(x1)))))) -> 2(1(4(1(3(3(2(2(5(4(x1)))))))))) 3(0(5(5(4(3(x1)))))) -> 3(3(0(3(2(3(5(5(1(0(x1)))))))))) 3(5(4(3(5(2(x1)))))) -> 2(0(5(2(0(5(2(2(3(2(x1)))))))))) 4(4(2(5(5(0(x1)))))) -> 4(4(0(0(3(3(3(2(2(3(x1)))))))))) 4(5(3(5(5(0(x1)))))) -> 4(2(2(3(0(2(4(1(1(5(x1)))))))))) 5(4(5(1(1(2(x1)))))) -> 5(4(0(3(3(3(3(2(5(5(x1)))))))))) 5(5(5(5(5(3(x1)))))) -> 5(5(0(1(4(0(0(5(0(1(x1)))))))))) 3(5(0(0(5(4(3(x1))))))) -> 0(1(2(1(1(5(5(2(1(0(x1)))))))))) 3(5(4(2(5(2(3(x1))))))) -> 4(0(4(0(0(2(2(3(4(4(x1)))))))))) 3(5(4(5(1(4(0(x1))))))) -> 1(1(1(0(0(3(3(1(2(5(x1)))))))))) Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {7} transitions: 11(277) -> 278* 11(60) -> 61* 11(247) -> 248* 11(30) -> 31* 11(25) -> 26* 11(20) -> 21* 11(192) -> 193* 11(62) -> 63* 11(456) -> 457* 11(254) -> 255* 11(52) -> 53* 11(239) -> 240* 11(391) -> 392* 11(159) -> 160* 11(124) -> 125* 11(59) -> 60* 11(216) -> 217* 11(191) -> 192* 11(186) -> 187* 11(161) -> 162* 11(151) -> 152* 11(61) -> 62* 11(455) -> 456* 11(450) -> 451* 11(36) -> 37* 11(31) -> 32* 11(213) -> 214* 11(208) -> 209* 11(158) -> 159* 11(78) -> 79* 11(457) -> 458* 11(245) -> 246* 11(240) -> 241* 11(38) -> 39* 11(28) -> 29* 11(554) -> 555* 11(125) -> 126* 01(282) -> 283* 01(454) -> 455* 01(162) -> 163* 01(152) -> 153* 01(117) -> 118* 01(77) -> 78* 01(32) -> 33* 01(27) -> 28* 01(426) -> 427* 01(416) -> 417* 01(214) -> 215* 01(189) -> 190* 01(558) -> 559* 01(149) -> 150* 01(139) -> 140* 01(84) -> 85* 01(453) -> 454* 01(49) -> 50* 01(443) -> 444* 01(241) -> 242* 01(34) -> 35* 01(211) -> 212* 01(393) -> 394* 01(181) -> 182* 01(146) -> 147* 01(116) -> 117* 01(445) -> 446* 01(243) -> 244* 01(26) -> 27* 01(395) -> 396* 01(183) -> 184* 01(148) -> 149* 01(128) -> 129* 01(108) -> 109* 01(442) -> 443* 01(23) -> 24* 01(215) -> 216* 01(190) -> 191* 01(180) -> 181* 01(105) -> 106* 31(75) -> 76* 31(50) -> 51* 31(242) -> 243* 31(439) -> 440* 31(414) -> 415* 31(212) -> 213* 31(389) -> 390* 31(187) -> 188* 31(177) -> 178* 31(137) -> 138* 31(57) -> 58* 31(451) -> 452* 31(129) -> 130* 31(114) -> 115* 31(74) -> 75* 31(24) -> 25* 31(418) -> 419* 31(413) -> 414* 31(136) -> 137* 31(101) -> 102* 31(86) -> 87* 31(283) -> 284* 31(81) -> 82* 31(56) -> 57* 31(415) -> 416* 31(410) -> 411* 31(390) -> 391* 31(188) -> 189* 31(138) -> 139* 31(113) -> 114* 31(83) -> 84* 31(63) -> 64* 31(452) -> 453* 31(33) -> 34* 31(135) -> 136* 31(115) -> 116* 31(110) -> 111* 31(85) -> 86* 21(459) -> 460* 21(449) -> 450* 21(45) -> 46* 21(207) -> 208* 21(127) -> 128* 21(112) -> 113* 21(102) -> 103* 21(82) -> 83* 21(72) -> 73* 21(441) -> 442* 21(411) -> 412* 21(179) -> 180* 21(134) -> 135* 21(39) -> 40* 21(19) -> 20* 21(388) -> 389* 21(131) -> 132* 21(111) -> 112* 21(106) -> 107* 21(278) -> 279* 21(248) -> 249* 21(440) -> 441* 21(178) -> 179* 21(103) -> 104* 21(73) -> 74* 21(412) -> 413* 21(185) -> 186* 21(160) -> 161* 21(155) -> 156* 21(130) -> 131* 51(80) -> 81* 51(55) -> 56* 51(424) -> 425* 51(566) -> 567* 51(157) -> 158* 51(147) -> 148* 51(516) -> 517* 51(107) -> 108* 51(279) -> 280* 51(209) -> 210* 51(518) -> 519* 51(104) -> 105* 51(79) -> 80* 51(448) -> 449* 51(156) -> 157* 51(71) -> 72* 51(46) -> 47* 51(21) -> 22* 51(420) -> 421* 51(153) -> 154* 51(552) -> 553* 51(133) -> 134* 51(58) -> 59* 51(53) -> 54* 51(422) -> 423* 51(494) -> 495* 41(70) -> 71* 41(444) -> 445* 41(35) -> 36* 41(182) -> 183* 41(284) -> 285* 41(47) -> 48* 41(446) -> 447* 41(244) -> 245* 41(37) -> 38* 41(22) -> 23* 41(281) -> 282* 41(64) -> 65* 41(246) -> 247* 41(438) -> 439* 41(176) -> 177* 41(126) -> 127* 41(51) -> 52* 41(118) -> 119* 41(280) -> 281* 41(48) -> 49* 41(437) -> 438* 41(210) -> 211* 41(150) -> 151* 41(140) -> 141* 42(541) -> 542* 42(511) -> 512* 42(548) -> 549* 42(550) -> 551* 42(525) -> 526* 42(490) -> 491* 42(542) -> 543* 42(512) -> 513* 20(7) -> 7* 02(546) -> 547* 02(521) -> 522* 02(523) -> 524* 02(510) -> 511* 02(547) -> 548* 02(527) -> 528* 02(549) -> 550* 02(524) -> 525* 02(509) -> 510* 50(7) -> 7* 22(545) -> 546* 22(505) -> 506* 22(544) -> 545* 22(504) -> 505* 30(7) -> 7* 32(489) -> 490* 32(556) -> 557* 32(506) -> 507* 32(543) -> 544* 32(508) -> 509* 32(503) -> 504* 32(483) -> 484* 32(562) -> 563* 32(507) -> 508* 32(482) -> 483* 32(514) -> 515* 00(7) -> 7* 52(484) -> 485* 52(481) -> 482* 52(528) -> 529* 52(522) -> 523* 52(492) -> 493* 52(529) -> 530* 10(7) -> 7* 12(526) -> 527* 12(486) -> 487* 12(488) -> 489* 12(520) -> 521* 12(485) -> 486* 12(487) -> 488* 40(7) -> 7* 7 -> 110,77,70,55,30,19 19 -> 516* 20 -> 7,77,55,19,30,70,110,388,101 29 -> 483,57,111,20,186,101,7 31 -> 146,45 39 -> 424* 40 -> 483,57,111,20,101,31,45,146,7 53 -> 492* 54 -> 517,134,72,56,133,124,185,7 55 -> 481* 56 -> 7,77,55,19,30,70,110,185,133,124 63 -> 393,239 65 -> 483,57,111,71,177,176,56,133,72,124,185,7 71 -> 7,176 76 -> 36* 79 -> 155* 86 -> 541,520,437,395,254 87 -> 111,7 109 -> 39* 113 -> 494* 119 -> 64* 132 -> 64* 141 -> 53* 152 -> 514,420,410 154 -> 53* 162 -> 503,422,418,277,207 163 -> 483,57,111,7 183 -> 448* 184 -> 64* 193 -> 28* 217 -> 20,186,7,101 248 -> 518* 249 -> 31,45,7,146 255 -> 426,240 285 -> 28* 392 -> 284* 394 -> 78* 396 -> 78* 417 -> 183* 419 -> 411* 421 -> 124* 423 -> 459,124 425 -> 133* 427 -> 147* 445 -> 552* 447 -> 57,7,77,55,19,30,70,110,111 458 -> 483,57,7,77,55,19,30,70,110,111 460 -> 450* 489 -> 558,554 491 -> 482,517,56,133,72,7,124,185 493 -> 482* 495 -> 105* 513 -> 71,177,7,176 515 -> 504* 517 -> 53* 519 -> 53* 527 -> 566,562 530 -> 493,54,492,482,556,56,133,134,7,124,185 551 -> 483,57,111 553 -> 185* 555 -> 31* 557 -> 483* 559 -> 78* 563 -> 504* 567 -> 124* problem: Qed