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