YES Problem: b(a(a(b(a(b(x1)))))) -> a(b(a(b(a(b(a(x1))))))) Proof: String Reversal Processor: b(a(b(a(a(b(x1)))))) -> a(b(a(b(a(b(a(x1))))))) Bounds Processor: bound: 3 enrichment: match automaton: final states: {3} transitions: a3(152) -> 153* a3(164) -> 165* a3(114) -> 115* a3(126) -> 127* a3(116) -> 117* a3(118) -> 119* a3(120) -> 121* a1(20) -> 21* a1(22) -> 23* a1(12) -> 13* a1(24) -> 25* a1(14) -> 15* a1(26) -> 27* a1(16) -> 17* a1(98) -> 99* a1(58) -> 59* a1(18) -> 19* a1(150) -> 151* b3(117) -> 118* b3(119) -> 120* b3(115) -> 116* b1(25) -> 26* b1(15) -> 16* b1(17) -> 18* b1(21) -> 22* b1(23) -> 24* b1(13) -> 14* a2(50) -> 51* a2(40) -> 41* a2(112) -> 113* a2(92) -> 93* a2(52) -> 53* a2(42) -> 43* a2(94) -> 95* a2(54) -> 55* a2(44) -> 45* a2(86) -> 87* a2(56) -> 57* a2(46) -> 47* a2(158) -> 159* a2(138) -> 139* a2(128) -> 129* a2(88) -> 89* a2(38) -> 39* a2(100) -> 101* a2(90) -> 91* b0(3) -> 3* b2(55) -> 56* b2(87) -> 88* b2(89) -> 90* b2(39) -> 40* b2(91) -> 92* b2(51) -> 52* b2(41) -> 42* b2(53) -> 54* b2(43) -> 44* a0(3) -> 3* 3 -> 12* 13 -> 86* 15 -> 50* 17 -> 38,20 19 -> 90,16,14,3 21 -> 138* 23 -> 112* 25 -> 46* 27 -> 3,12,14 39 -> 126* 41 -> 114,100 43 -> 94,58 45 -> 18,14,3,16 47 -> 39* 51 -> 152* 53 -> 128* 55 -> 98* 57 -> 42,24 59 -> 13* 93 -> 54* 95 -> 39* 99 -> 13* 101 -> 39* 113 -> 51* 115 -> 164* 117 -> 158* 119 -> 150* 121 -> 118,42 127 -> 115* 129 -> 39* 139 -> 87* 151 -> 13* 153 -> 115* 159 -> 39* 165 -> 115* problem: Qed