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