Problem: ap(ap(g(),x),y) -> y ap(f(),x) -> ap(f(),app(g(),x)) Proof: Containment Processor: loop length: 1 terms: ap(f(),x) context: [] substitution: x -> app(g(),x) Qed