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)) Usable Rule Processor: DPs: f#(g(f(X))) -> f#(g(X)) TRS: Bounds Processor: bound: 1 enrichment: match automaton: final states: {6} transitions: f{#,1}(11) -> 12* g1(10) -> 11* g1(13) -> 14* f{#,0}(5) -> 6* f{#,0}(4) -> 6* g0(5) -> 4* g0(4) -> 4* f0(5) -> 5* f0(4) -> 5* 4 -> 13* 5 -> 10* 12 -> 6* 14 -> 11* problem: DPs: TRS: Qed