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