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