MAYBE Problem: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(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),s(y)) -> f#(x,s(c(s(y)))) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) EDG Processor: DPs: f#(x,c(y)) -> f#(y,y) f#(x,c(y)) -> f#(x,s(f(y,y))) f#(s(x),s(y)) -> f#(x,s(c(s(y)))) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) graph: f#(s(x),s(y)) -> f#(x,s(c(s(y)))) -> f#(s(x),s(y)) -> f#(x,s(c(s(y)))) f#(x,c(y)) -> f#(y,y) -> f#(x,c(y)) -> f#(y,y) f#(x,c(y)) -> f#(y,y) -> f#(x,c(y)) -> f#(x,s(f(y,y))) f#(x,c(y)) -> f#(y,y) -> f#(s(x),s(y)) -> f#(x,s(c(s(y)))) f#(x,c(y)) -> f#(x,s(f(y,y))) -> f#(s(x),s(y)) -> f#(x,s(c(s(y)))) SCC Processor: #sccs: 2 #rules: 2 #arcs: 5/9 DPs: f#(x,c(y)) -> f#(y,y) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) Open DPs: f#(s(x),s(y)) -> f#(x,s(c(s(y)))) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) Open