YES Problem: 4(2(4(x1))) -> 2(0(0(5(3(3(5(2(0(4(x1)))))))))) 4(4(2(4(2(x1))))) -> 2(0(5(2(1(4(0(2(0(1(x1)))))))))) 0(5(4(2(4(3(x1)))))) -> 5(1(5(5(3(5(3(0(0(0(x1)))))))))) 1(1(4(5(3(3(x1)))))) -> 1(3(1(1(3(0(1(2(2(1(x1)))))))))) 3(1(4(3(1(2(x1)))))) -> 0(0(1(1(4(2(3(0(0(3(x1)))))))))) 3(2(4(2(4(1(x1)))))) -> 0(2(1(1(1(5(3(1(3(3(x1)))))))))) 3(3(0(4(1(2(x1)))))) -> 3(5(1(2(0(2(0(5(3(1(x1)))))))))) 4(1(4(5(0(5(4(x1))))))) -> 4(1(5(3(1(0(5(3(1(0(x1)))))))))) 4(4(0(5(4(2(2(x1))))))) -> 4(0(4(3(4(4(4(5(4(1(x1)))))))))) 5(4(5(3(2(4(3(x1))))))) -> 2(5(5(5(0(4(5(0(1(4(x1)))))))))) Proof: String Reversal Processor: 4(2(4(x1))) -> 4(0(2(5(3(3(5(0(0(2(x1)))))))))) 2(4(2(4(4(x1))))) -> 1(0(2(0(4(1(2(5(0(2(x1)))))))))) 3(4(2(4(5(0(x1)))))) -> 0(0(0(3(5(3(5(5(1(5(x1)))))))))) 3(3(5(4(1(1(x1)))))) -> 1(2(2(1(0(3(1(1(3(1(x1)))))))))) 2(1(3(4(1(3(x1)))))) -> 3(0(0(3(2(4(1(1(0(0(x1)))))))))) 1(4(2(4(2(3(x1)))))) -> 3(3(1(3(5(1(1(1(2(0(x1)))))))))) 2(1(4(0(3(3(x1)))))) -> 1(3(5(0(2(0(2(1(5(3(x1)))))))))) 4(5(0(5(4(1(4(x1))))))) -> 0(1(3(5(0(1(3(5(1(4(x1)))))))))) 2(2(4(5(0(4(4(x1))))))) -> 1(4(5(4(4(4(3(4(0(4(x1)))))))))) 3(4(2(3(5(4(5(x1))))))) -> 4(1(0(5(4(0(5(5(5(2(x1)))))))))) Bounds Processor: bound: 1 enrichment: match automaton: final states: {7} transitions: 41(137) -> 138* 41(72) -> 73* 41(204) -> 205* 41(139) -> 140* 41(109) -> 110* 41(271) -> 272* 41(136) -> 137* 41(133) -> 134* 41(33) -> 34* 41(28) -> 29* 41(145) -> 146* 41(135) -> 136* 11(80) -> 81* 11(70) -> 71* 11(60) -> 61* 11(117) -> 118* 11(82) -> 83* 11(269) -> 270* 11(57) -> 58* 11(37) -> 38* 11(32) -> 33* 11(331) -> 332* 11(326) -> 327* 11(261) -> 262* 11(54) -> 55* 11(44) -> 45* 11(353) -> 354* 11(328) -> 329* 11(101) -> 102* 11(81) -> 82* 11(71) -> 72* 11(56) -> 57* 11(208) -> 209* 11(203) -> 204* 11(148) -> 149* 11(113) -> 114* 11(270) -> 271* 11(357) -> 358* 11(327) -> 328* 11(110) -> 111* 11(85) -> 86* 01(282) -> 283* 01(75) -> 76* 01(267) -> 268* 01(50) -> 51* 01(20) -> 21* 01(207) -> 208* 01(354) -> 355* 01(147) -> 148* 01(132) -> 133* 01(274) -> 275* 01(52) -> 53* 01(27) -> 28* 01(381) -> 382* 01(144) -> 145* 01(114) -> 115* 01(69) -> 70* 01(59) -> 60* 01(34) -> 35* 01(383) -> 384* 01(358) -> 359* 01(156) -> 157* 01(76) -> 77* 01(268) -> 269* 01(51) -> 52* 01(36) -> 37* 01(21) -> 22* 01(103) -> 104* 01(275) -> 276* 01(68) -> 69* 01(205) -> 206* 01(155) -> 156* 01(105) -> 106* 51(45) -> 46* 51(30) -> 31* 51(25) -> 26* 51(379) -> 380* 51(157) -> 158* 51(142) -> 143* 51(329) -> 330* 51(22) -> 23* 51(246) -> 247* 51(201) -> 202* 51(348) -> 349* 51(146) -> 147* 51(141) -> 142* 51(111) -> 112* 51(106) -> 107* 51(46) -> 47* 51(395) -> 396* 51(355) -> 356* 51(143) -> 144* 51(138) -> 139* 51(83) -> 84* 51(48) -> 49* 51(43) -> 44* 51(160) -> 161* 51(115) -> 116* 51(100) -> 101* 21(272) -> 273* 21(35) -> 36* 21(202) -> 203* 21(102) -> 103* 21(62) -> 63* 21(154) -> 155* 21(104) -> 105* 21(79) -> 80* 21(19) -> 20* 21(206) -> 207* 21(161) -> 162* 21(61) -> 62* 21(31) -> 32* 21(26) -> 27* 21(350) -> 351* 21(325) -> 326* 21(73) -> 74* 21(377) -> 378* 31(55) -> 56* 31(112) -> 113* 31(107) -> 108* 31(77) -> 78* 31(47) -> 48* 31(159) -> 160* 31(356) -> 357* 31(134) -> 135* 31(99) -> 100* 31(84) -> 85* 31(276) -> 277* 31(74) -> 75* 31(49) -> 50* 31(24) -> 25* 31(333) -> 334* 31(116) -> 117* 31(86) -> 87* 31(273) -> 274* 31(158) -> 159* 31(330) -> 331* 31(58) -> 59* 31(23) -> 24* 31(352) -> 353* 31(332) -> 333* 40(7) -> 7* 20(7) -> 7* 00(7) -> 7* 50(7) -> 7* 30(7) -> 7* 10(7) -> 7* 7 -> 109,99,68,54,43,19 20 -> 141* 21 -> 30* 28 -> 154* 29 -> 100,110,132,7 38 -> 378,100,20,141,7 44 -> 352* 45 -> 350* 52 -> 246* 53 -> 110,132,100,7 63 -> 37* 69 -> 79* 77 -> 282* 78 -> 378,55,111,20,141,7 87 -> 348,77 100 -> 261* 107 -> 267* 108 -> 37* 109 -> 377* 110 -> 7,99,54,19,43,68,109,132 118 -> 52* 140 -> 37* 149 -> 28* 156 -> 201* 162 -> 52* 209 -> 378,20,7,99,54,19,43,68,109,141 247 -> 44* 262 -> 57* 276 -> 381* 277 -> 378,20,7,99,54,19,43,68,109,141 283 -> 325,268 333 -> 395,383 334 -> 55,7,99,54,19,43,68,109,111 349 -> 101* 351 -> 103* 358 -> 379* 359 -> 110,7,99,54,19,43,68,109,132 378 -> 20* 380 -> 44* 382 -> 69* 384 -> 69* 396 -> 44* problem: Qed