NO Problem: strict: b(a(x)) -> a(b(x)) weak: a(x) -> a(a(x)) b(x) -> b(b(x)) Proof: Unfolding Processor: loop length: 2 terms: b(a(x16)) b(b(a(x16))) context: [] substitution: x16 -> b(x16) Qed