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