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