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