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