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