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