MAYBE Problem: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Proof: DP Processor: DPs: f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) h#(x,x) -> g#(x,0()) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) EDG Processor: DPs: f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) h#(x,x) -> g#(x,0()) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) graph: f#(f(x)) -> h#(f(x),f(x)) -> h#(x,x) -> g#(x,0()) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) -> f#(f(x)) -> f#(h(f(x),f(x))) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(g(f(x),x)) -> f#(f(x)) -> f#(h(f(x),f(x))) Restore Modifier: DPs: f#(f(x)) -> g#(f(x),x) f#(f(x)) -> f#(g(f(x),x)) f#(f(x)) -> h#(f(x),f(x)) f#(f(x)) -> f#(h(f(x),f(x))) h#(x,x) -> g#(x,0()) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) SCC Processor: #sccs: 1 #rules: 2 #arcs: 9/25 DPs: f#(f(x)) -> f#(h(f(x),f(x))) f#(f(x)) -> f#(g(f(x),x)) TRS: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Open