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