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