NO Problem: g(f(a())) -> f(g(f(a()))) g(f(a())) -> f(f(a())) f(f(a())) -> f(a()) Proof: Containment Processor: loop length: 1 terms: g(f(a())) context: f([]) substitution: Qed