YES Problem: 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1)))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {40,33,26,19,12,1} transitions: 11(65) -> 66* 11(197) -> 198* 11(192) -> 193* 11(142) -> 143* 11(137) -> 138* 11(117) -> 118* 11(67) -> 68* 11(62) -> 63* 11(194) -> 195* 11(189) -> 190* 11(169) -> 170* 11(119) -> 120* 11(114) -> 115* 11(64) -> 65* 11(59) -> 60* 11(171) -> 172* 11(166) -> 167* 11(116) -> 117* 11(111) -> 112* 11(91) -> 92* 11(168) -> 169* 11(163) -> 164* 11(143) -> 144* 11(93) -> 94* 11(88) -> 89* 11(195) -> 196* 11(145) -> 146* 11(140) -> 141* 11(90) -> 91* 11(85) -> 86* 21(207) -> 208* 21(162) -> 163* 21(147) -> 148* 21(92) -> 93* 21(87) -> 88* 21(219) -> 220* 21(199) -> 200* 21(144) -> 145* 21(139) -> 140* 21(84) -> 85* 21(69) -> 70* 21(211) -> 212* 21(196) -> 197* 21(191) -> 192* 21(136) -> 137* 21(121) -> 122* 21(66) -> 67* 21(61) -> 62* 21(203) -> 204* 21(188) -> 189* 21(173) -> 174* 21(118) -> 119* 21(113) -> 114* 21(58) -> 59* 21(215) -> 216* 21(170) -> 171* 21(165) -> 166* 21(110) -> 111* 21(95) -> 96* 01(60) -> 61* 01(167) -> 168* 01(112) -> 113* 01(164) -> 165* 01(89) -> 90* 01(141) -> 142* 01(86) -> 87* 01(193) -> 194* 01(138) -> 139* 01(63) -> 64* 01(190) -> 191* 01(115) -> 116* f30() -> 2* 10(30) -> 31* 10(25) -> 19* 10(20) -> 21* 10(15) -> 16* 10(37) -> 38* 10(32) -> 26* 10(27) -> 28* 10(22) -> 23* 10(44) -> 45* 10(39) -> 33* 10(34) -> 35* 10(29) -> 30* 10(9) -> 10* 10(46) -> 40* 10(41) -> 42* 10(36) -> 37* 10(16) -> 17* 10(11) -> 1* 10(6) -> 7* 10(43) -> 44* 10(23) -> 24* 10(18) -> 12* 10(13) -> 14* 10(8) -> 9* 10(3) -> 4* 20(45) -> 46* 20(15) -> 20* 20(10) -> 11* 20(5) -> 6* 20(22) -> 27* 20(17) -> 18* 20(2) -> 3* 20(29) -> 34* 20(24) -> 25* 20(36) -> 41* 20(31) -> 32* 20(38) -> 39* 20(8) -> 13* 00(35) -> 36* 00(42) -> 43* 00(7) -> 8* 00(14) -> 15* 00(4) -> 5* 00(21) -> 22* 00(28) -> 29* 1 -> 5* 11 -> 58* 12 -> 5* 18 -> 203* 19 -> 5* 25 -> 207* 26 -> 5* 32 -> 211* 33 -> 5* 39 -> 215* 40 -> 5* 46 -> 219* 64 -> 69* 67 -> 84* 68 -> 8* 70 -> 62* 90 -> 95* 93 -> 110* 94 -> 15* 96 -> 88* 116 -> 121* 119 -> 136* 120 -> 22* 122 -> 114* 142 -> 147* 145 -> 162* 146 -> 29* 148 -> 140* 168 -> 173* 171 -> 188* 172 -> 36* 174 -> 166* 194 -> 199* 198 -> 43* 200 -> 192* 204 -> 59* 208 -> 59* 212 -> 59* 216 -> 59* 220 -> 59* problem: Qed