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