NO Problem: I(x) -> I(J(x)) J(x) -> J(K(J(x))) H(I(x)) -> K(J(x)) J(x) -> K(J(x)) Proof: Containment Processor: loop length: 1 terms: I(x) context: [] substitution: x -> J(x) Qed