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