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)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {4} transitions: f{#,0}(5) -> 4* g0(2) -> 2* g0(1) -> 2* g0(3) -> 5* f0(2) -> 1* f0(1) -> 1* f{#,1}(10) -> 11* g1(12) -> 13* g1(9) -> 10* 1 -> 12,3 2 -> 9,3 11 -> 4* 13 -> 10* problem: DPs: TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) Qed