MAYBE Problem: f(g(x),x,y) -> f(y,y,g(y)) g(g(x)) -> g(x) Proof: DP Processor: DPs: f#(g(x),x,y) -> g#(y) f#(g(x),x,y) -> f#(y,y,g(y)) TRS: f(g(x),x,y) -> f(y,y,g(y)) g(g(x)) -> g(x) Usable Rule Processor: DPs: f#(g(x),x,y) -> g#(y) f#(g(x),x,y) -> f#(y,y,g(y)) TRS: f4(x,y) -> x f4(x,y) -> y g(g(x)) -> g(x) TDG Processor: DPs: f#(g(x),x,y) -> g#(y) f#(g(x),x,y) -> f#(y,y,g(y)) TRS: f4(x,y) -> x f4(x,y) -> y g(g(x)) -> g(x) graph: f#(g(x),x,y) -> f#(y,y,g(y)) -> f#(g(x),x,y) -> f#(y,y,g(y)) f#(g(x),x,y) -> f#(y,y,g(y)) -> f#(g(x),x,y) -> g#(y) Restore Modifier: DPs: f#(g(x),x,y) -> g#(y) f#(g(x),x,y) -> f#(y,y,g(y)) TRS: f(g(x),x,y) -> f(y,y,g(y)) g(g(x)) -> g(x) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: f#(g(x),x,y) -> f#(y,y,g(y)) TRS: f(g(x),x,y) -> f(y,y,g(y)) g(g(x)) -> g(x) Open