NO Problem: b(b(b(x1))) -> a(a(x1)) a(a(x1)) -> b(a(b(x1))) Proof: Unfolding Processor: loop length: 6 terms: a(a(b(b(a(b(b(a(x664)))))))) b(a(b(b(b(a(b(b(a(x664))))))))) b(a(a(a(a(b(b(a(x664)))))))) b(a(a(b(a(b(b(b(a(x664))))))))) b(a(a(b(a(a(a(a(x664)))))))) b(a(a(b(b(a(b(a(a(x664))))))))) context: b([]) substitution: x664 -> b(x664) Qed