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))))))))))))) 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))))))))))))) Bounds Processor: bound: 2 enrichment: match automaton: final states: {12,1} transitions: 21(35) -> 36* 21(32) -> 33* 21(27) -> 28* 21(61) -> 62* 21(58) -> 59* 21(53) -> 54* 11(60) -> 61* 11(55) -> 56* 11(112) -> 113* 11(57) -> 58* 11(52) -> 53* 11(54) -> 55* 11(34) -> 35* 11(29) -> 30* 11(31) -> 32* 11(26) -> 27* 11(28) -> 29* 01(30) -> 31* 01(37) -> 38* 01(59) -> 60* 01(56) -> 57* 01(63) -> 64* 01(33) -> 34* 22(87) -> 88* 22(84) -> 85* 22(79) -> 80* 12(80) -> 81* 12(89) -> 90* 12(86) -> 87* 12(81) -> 82* 12(108) -> 109* 12(83) -> 84* 12(78) -> 79* f30() -> 2* 02(82) -> 83* 02(95) -> 96* 02(85) -> 86* 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(4) -> 5* 10(13) -> 14* 00(9) -> 10* 00(6) -> 7* 00(1) -> 13* 1 -> 112,3,5 6 -> 52* 9 -> 26* 12 -> 3,5 30 -> 108* 33 -> 89* 36 -> 113,27,37,6 37 -> 78* 38 -> 34* 62 -> 63,27 64 -> 60* 88 -> 90,79,95,53 90 -> 79* 96 -> 86* 109 -> 79* 113 -> 27* problem: Qed