YES Problem: f(f(a())) -> f(g()) Proof: DP Processor: DPs: f#(f(a())) -> f#(g()) TRS: f(f(a())) -> f(g()) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(f(a())) -> f#(g()) TRS: f(f(a())) -> f(g()) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0, [g] = 0, [f](x0) = 1, [a] = 0 orientation: f#(f(a())) = 1 >= 0 = f#(g()) f(f(a())) = 1 >= 1 = f(g()) problem: DPs: TRS: f(f(a())) -> f(g()) Qed