MAYBE 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)) Restore Modifier: 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)) SCC Processor: #sccs: 1 #rules: 3 #arcs: 9/9 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0, [g](x0) = 0, [f](x0) = 1 orientation: f#(f(X)) = 1 >= 0 = f#(g(f(X))) f#(f(X)) = 1 >= 0 = f#(g(f(g(f(X))))) f#(g(f(X))) = 0 >= 0 = f#(g(X)) f(f(X)) = 1 >= 1 = f(g(f(g(f(X))))) f(g(f(X))) = 1 >= 1 = f(g(X)) problem: 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)) Open