YES Problem: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) Proof: DP Processor: DPs: f#(f(X)) -> f#(g(f(X))) f#(f(X)) -> f#(g(f(g(f(X))))) f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) EDG Processor: DPs: f#(f(X)) -> f#(g(f(X))) f#(f(X)) -> f#(g(f(g(f(X))))) f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) graph: f#(g(f(X))) -> f#(g(X)) -> f#(g(f(X))) -> f#(g(X)) f#(f(X)) -> f#(g(f(g(f(X))))) -> f#(g(f(X))) -> f#(g(X)) f#(f(X)) -> f#(g(f(X))) -> f#(g(f(X))) -> f#(g(X)) CDG Processor: DPs: f#(f(X)) -> f#(g(f(X))) f#(f(X)) -> f#(g(f(g(f(X))))) f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) graph: f#(f(X)) -> f#(g(f(g(f(X))))) -> f#(g(f(X))) -> f#(g(X)) f#(f(X)) -> f#(g(f(X))) -> f#(g(f(X))) -> f#(g(X)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/9