NO Problem: a(b(a(b(x)))) -> b(a(b(a(a(b(x)))))) Proof: String Reversal Processor: b(a(b(a(x)))) -> b(a(a(b(a(b(x)))))) Unfolding Processor: loop length: 2 terms: b(a(b(a(a(b(a(x10))))))) b(a(a(b(a(b(a(b(a(x10))))))))) context: b(a(a([]))) substitution: x10 -> b(x10) Qed