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