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