YES Problem: b(c(a(b(b(c(x1)))))) -> a(b(c(b(b(c(a(x1))))))) Proof: String Reversal Processor: c(b(b(a(c(b(x1)))))) -> a(c(b(b(c(b(a(x1))))))) Bounds Processor: bound: 0 enrichment: match automaton: final states: {1} transitions: f30() -> 2* a0(2) -> 3* a0(8) -> 1* c0(7) -> 8* c0(4) -> 5* b0(5) -> 6* b0(6) -> 7* b0(3) -> 4* problem: Qed