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