MAYBE Problem: g(x,y) -> x g(x,y) -> y f(0(),1(),x) -> f(s(x),x,x) f(x,y,s(z)) -> s(f(0(),1(),z)) Proof: DP Processor: DPs: f#(0(),1(),x) -> f#(s(x),x,x) f#(x,y,s(z)) -> f#(0(),1(),z) TRS: g(x,y) -> x g(x,y) -> y f(0(),1(),x) -> f(s(x),x,x) f(x,y,s(z)) -> s(f(0(),1(),z)) ADG Processor: DPs: f#(0(),1(),x) -> f#(s(x),x,x) f#(x,y,s(z)) -> f#(0(),1(),z) TRS: g(x,y) -> x g(x,y) -> y f(0(),1(),x) -> f(s(x),x,x) f(x,y,s(z)) -> s(f(0(),1(),z)) graph: f#(0(),1(),x) -> f#(s(x),x,x) -> f#(x,y,s(z)) -> f#(0(),1(),z) f#(x,y,s(z)) -> f#(0(),1(),z) -> f#(0(),1(),x) -> f#(s(x),x,x) f#(x,y,s(z)) -> f#(0(),1(),z) -> f#(x,y,s(z)) -> f#(0(),1(),z) SCC Processor: #sccs: 1 #rules: 2 #arcs: 3/4 DPs: f#(0(),1(),x) -> f#(s(x),x,x) f#(x,y,s(z)) -> f#(0(),1(),z) TRS: g(x,y) -> x g(x,y) -> y f(0(),1(),x) -> f(s(x),x,x) f(x,y,s(z)) -> s(f(0(),1(),z)) Open