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))))))))))))))))))))))))) 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(0(1(2(x1)))))))))))))))))))))))))))) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {47,40,33,26,19,12,1} transitions: 11(227) -> 228* 11(222) -> 223* 11(202) -> 203* 11(152) -> 153* 11(147) -> 148* 11(97) -> 98* 11(92) -> 93* 11(72) -> 73* 11(204) -> 205* 11(199) -> 200* 11(149) -> 150* 11(144) -> 145* 11(124) -> 125* 11(74) -> 75* 11(69) -> 70* 11(201) -> 202* 11(196) -> 197* 11(176) -> 177* 11(126) -> 127* 11(121) -> 122* 11(71) -> 72* 11(66) -> 67* 11(228) -> 229* 11(178) -> 179* 11(173) -> 174* 11(123) -> 124* 11(118) -> 119* 11(98) -> 99* 11(230) -> 231* 11(225) -> 226* 11(175) -> 176* 11(170) -> 171* 11(150) -> 151* 11(100) -> 101* 11(95) -> 96* 21(65) -> 66* 21(252) -> 253* 21(232) -> 233* 21(177) -> 178* 21(172) -> 173* 21(117) -> 118* 21(102) -> 103* 21(244) -> 245* 21(229) -> 230* 21(224) -> 225* 21(169) -> 170* 21(154) -> 155* 21(99) -> 100* 21(94) -> 95* 21(256) -> 257* 21(236) -> 237* 21(221) -> 222* 21(206) -> 207* 21(151) -> 152* 21(146) -> 147* 21(91) -> 92* 21(76) -> 77* 21(248) -> 249* 21(203) -> 204* 21(198) -> 199* 21(143) -> 144* 21(128) -> 129* 21(73) -> 74* 21(68) -> 69* 21(240) -> 241* 21(195) -> 196* 21(180) -> 181* 21(125) -> 126* 21(120) -> 121* 01(70) -> 71* 01(197) -> 198* 01(122) -> 123* 01(67) -> 68* 01(174) -> 175* 01(119) -> 120* 01(226) -> 227* 01(171) -> 172* 01(96) -> 97* 01(223) -> 224* 01(148) -> 149* 01(93) -> 94* 01(200) -> 201* 01(145) -> 146* f30() -> 2* 10(50) -> 51* 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(51) -> 52* 10(46) -> 40* 10(41) -> 42* 10(36) -> 37* 10(16) -> 17* 10(11) -> 1* 10(6) -> 7* 10(53) -> 47* 10(48) -> 49* 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(52) -> 53* 20(22) -> 27* 20(17) -> 18* 20(2) -> 3* 20(29) -> 34* 20(24) -> 25* 20(36) -> 41* 20(31) -> 32* 20(43) -> 48* 20(38) -> 39* 20(8) -> 13* 00(35) -> 36* 00(42) -> 43* 00(7) -> 8* 00(49) -> 50* 00(14) -> 15* 00(4) -> 5* 00(21) -> 22* 00(28) -> 29* 1 -> 5* 11 -> 65* 12 -> 5* 18 -> 236* 19 -> 5* 25 -> 240* 26 -> 5* 32 -> 244* 33 -> 5* 39 -> 248* 40 -> 5* 46 -> 252* 47 -> 5* 53 -> 256* 71 -> 76* 74 -> 91* 75 -> 8* 77 -> 69* 97 -> 102* 100 -> 117* 101 -> 15* 103 -> 95* 123 -> 128* 126 -> 143* 127 -> 22* 129 -> 121* 149 -> 154* 152 -> 169* 153 -> 29* 155 -> 147* 175 -> 180* 178 -> 195* 179 -> 36* 181 -> 173* 201 -> 206* 204 -> 221* 205 -> 43* 207 -> 199* 227 -> 232* 231 -> 50* 233 -> 225* 237 -> 66* 241 -> 66* 245 -> 66* 249 -> 66* 253 -> 66* 257 -> 66* problem: Qed