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