YES Problem: c() -> f() f() -> g() Proof: DP Processor: DPs: c#() -> f#() TRS: c() -> f() f() -> g() Usable Rule Processor: DPs: c#() -> f#() TRS: CDG Processor: DPs: c#() -> f#() TRS: graph: Qed