YES 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)))) Restore Modifier: 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)))) 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),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)))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x1 + 1, [s](x0) = 1, [f](x0, x1) = 0, [c](x0) = x0 + 1 orientation: f#(x,c(y)) = y + 2 >= y + 1 = f#(y,y) f#(x,c(y)) = y + 2 >= 2 = f#(x,s(f(y,y))) f#(s(x),s(y)) = 2 >= 2 = f#(x,s(c(s(y)))) f(x,c(y)) = 0 >= 0 = f(x,s(f(y,y))) f(s(x),s(y)) = 0 >= 0 = f(x,s(c(s(y)))) problem: DPs: 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)))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x1, [s](x0) = 0, [f](x0, x1) = 0, [c](x0) = 1 orientation: f#(x,c(y)) = 1 >= 0 = f#(x,s(f(y,y))) f#(s(x),s(y)) = 0 >= 0 = f#(x,s(c(s(y)))) f(x,c(y)) = 0 >= 0 = f(x,s(f(y,y))) f(s(x),s(y)) = 0 >= 0 = f(x,s(c(s(y)))) problem: 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)))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0, [s](x0) = x0 + 1, [f](x0, x1) = 0, [c](x0) = x0 orientation: f#(s(x),s(y)) = x + 1 >= x = f#(x,s(c(s(y)))) f(x,c(y)) = 0 >= 0 = f(x,s(f(y,y))) f(s(x),s(y)) = 0 >= 0 = f(x,s(c(s(y)))) problem: DPs: TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),s(y)) -> f(x,s(c(s(y)))) Qed