YES Problem: a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1))))))))) Proof: String Reversal Processor: a(b(a(a(b(a(a(x1))))))) -> b(a(a(a(b(a(a(b(a(x1))))))))) Bounds Processor: bound: 3 enrichment: match automaton: final states: {3} transitions: b3(222) -> 223* b3(194) -> 195* b3(191) -> 192* b3(156) -> 157* b3(198) -> 199* b3(153) -> 154* b3(220) -> 221* b3(160) -> 161* b1(15) -> 16* b1(27) -> 28* b1(22) -> 23* b1(84) -> 85* b1(24) -> 25* b1(176) -> 177* b1(31) -> 32* b1(18) -> 19* a3(197) -> 198* a3(192) -> 193* a3(157) -> 158* a3(152) -> 153* a3(214) -> 215* a3(159) -> 160* a3(154) -> 155* a3(196) -> 197* a3(193) -> 194* a3(158) -> 159* a3(200) -> 201* a3(195) -> 196* a3(190) -> 191* a3(155) -> 156* a1(30) -> 31* a1(25) -> 26* a1(20) -> 21* a1(17) -> 18* a1(29) -> 30* a1(19) -> 20* a1(14) -> 15* a1(26) -> 27* a1(21) -> 22* a1(16) -> 17* a1(28) -> 29* b2(45) -> 46* b2(212) -> 213* b2(112) -> 113* b2(102) -> 103* b2(87) -> 88* b2(52) -> 53* b2(204) -> 205* b2(174) -> 175* b2(109) -> 110* b2(99) -> 100* b2(94) -> 95* b2(206) -> 207* b2(136) -> 137* b2(116) -> 117* b2(106) -> 107* b2(133) -> 134* b2(128) -> 129* b2(48) -> 49* b2(140) -> 141* b2(90) -> 91* a0(3) -> 3* a2(50) -> 51* a2(137) -> 138* a2(132) -> 133* a2(92) -> 93* a2(47) -> 48* a2(139) -> 140* a2(134) -> 135* a2(114) -> 115* a2(104) -> 105* a2(89) -> 90* a2(49) -> 50* a2(44) -> 45* a2(111) -> 112* a2(101) -> 102* a2(91) -> 92* a2(86) -> 87* a2(51) -> 52* a2(46) -> 47* a2(138) -> 139* a2(113) -> 114* a2(108) -> 109* a2(103) -> 104* a2(98) -> 99* a2(93) -> 94* a2(88) -> 89* a2(135) -> 136* a2(115) -> 116* a2(110) -> 111* a2(105) -> 106* a2(100) -> 101* b0(3) -> 3* 3 -> 14* 16 -> 98* 19 -> 86* 20 -> 44* 21 -> 24* 23 -> 87,99,20,17,15,3 25 -> 132* 28 -> 108* 30 -> 84* 32 -> 99,17,3,15 47 -> 212* 50 -> 204* 51 -> 176* 53 -> 22,3,14,45,15,18,21 85 -> 16* 88 -> 190* 91 -> 152* 93 -> 128* 95 -> 109,50,29 107 -> 133,47,26 110 -> 214* 113 -> 200* 115 -> 174* 117 -> 87,20 129 -> 46* 141 -> 99,17 155 -> 222* 158 -> 220* 159 -> 206* 161 -> 50* 175 -> 46* 177 -> 16* 199 -> 47* 201 -> 153* 205 -> 110* 207 -> 46* 213 -> 134* 215 -> 191* 221 -> 154* 223 -> 192* problem: Qed