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