NO Problem: h(f(f(x))) -> h(f(g(f(x)))) f(g(f(x))) -> f(f(x)) Proof: Unfolding Processor: loop length: 2 terms: h(f(f(x8))) h(f(g(f(x8)))) context: [] substitution: x8 -> x8 Qed