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