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() Usable Rule Processor: DPs: f#(f(X)) -> c#() h#(X) -> c#() TRS: EDG Processor: DPs: f#(f(X)) -> c#() h#(X) -> c#() TRS: graph: Qed