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))))))))))))))))))) Proof: String Reversal Processor: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) Bounds Processor: bound: 2 enrichment: match automaton: final states: {18,15,12,1} transitions: f30() -> 2* 20(20) -> 18* 20(17) -> 15* 20(14) -> 12* 20(11) -> 1* 20(8) -> 9* 20(3) -> 4* 10(10) -> 11* 10(5) -> 6* 10(7) -> 8* 10(2) -> 3* 10(19) -> 20* 10(4) -> 5* 10(16) -> 17* 10(13) -> 14* 00(15) -> 19* 00(12) -> 16* 00(9) -> 10* 00(6) -> 7* 00(1) -> 13* 21(30) -> 31* 21(27) -> 28* 21(22) -> 23* 21(56) -> 57* 21(53) -> 54* 21(48) -> 49* 11(55) -> 56* 11(50) -> 51* 11(122) -> 123* 11(52) -> 53* 11(47) -> 48* 11(49) -> 50* 11(29) -> 30* 11(24) -> 25* 11(126) -> 127* 11(26) -> 27* 11(21) -> 22* 11(118) -> 119* 11(23) -> 24* 01(45) -> 46* 01(25) -> 26* 01(54) -> 55* 01(71) -> 72* 01(51) -> 52* 01(28) -> 29* 22(82) -> 83* 22(79) -> 80* 22(74) -> 75* 12(75) -> 76* 12(97) -> 98* 12(114) -> 115* 12(81) -> 82* 12(76) -> 77* 12(78) -> 79* 12(73) -> 74* 02(80) -> 81* 02(77) -> 78* 02(99) -> 100* 1 -> 118,3,5 6 -> 47* 9 -> 21* 12 -> 122,3,5 15 -> 126,3,5 18 -> 3,5 25 -> 114* 28 -> 97* 31 -> 127,123,119,45,6 45 -> 73* 46 -> 29* 57 -> 71,22 72 -> 55* 83 -> 98,74,99,48 98 -> 74* 100 -> 81* 115 -> 74* 119 -> 22* 123 -> 22* 127 -> 22* problem: Qed