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