YES Problem: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Proof: DP Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) TDG Processor: DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) graph: g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(s(f(x))) -> g#(f(x)) g#(c(x,s(y))) -> g#(c(s(x),y)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) -> g#(s(f(x))) -> g#(f(x)) g#(s(f(x))) -> g#(f(x)) -> g#(c(x,s(y))) -> g#(c(s(x),y)) f#(c(s(x),y)) -> f#(c(x,s(y))) -> f#(c(s(x),y)) -> f#(c(x,s(y))) SCC Processor: #sccs: 2 #rules: 3 #arcs: 5/9 DPs: f#(c(s(x),y)) -> f#(c(x,s(y))) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0, [g](x0) = 0, [f](x0) = 0, [c](x0, x1) = x0, [s](x0) = x0 + 1 orientation: f#(c(s(x),y)) = x + 1 >= x = f#(c(x,s(y))) f(c(s(x),y)) = 0 >= 0 = f(c(x,s(y))) g(c(x,s(y))) = 0 >= 0 = g(c(s(x),y)) g(s(f(x))) = 0 >= 0 = g(f(x)) problem: DPs: TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Qed DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) g#(s(f(x))) -> g#(f(x)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0, [g](x0) = 0, [f](x0) = 0, [c](x0, x1) = 0, [s](x0) = 1 orientation: g#(c(x,s(y))) = 0 >= 0 = g#(c(s(x),y)) g#(s(f(x))) = 1 >= 0 = g#(f(x)) f(c(s(x),y)) = 0 >= 0 = f(c(x,s(y))) g(c(x,s(y))) = 0 >= 0 = g(c(s(x),y)) g(s(f(x))) = 0 >= 0 = g(f(x)) problem: DPs: g#(c(x,s(y))) -> g#(c(s(x),y)) TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0, [g](x0) = 0, [f](x0) = 0, [c](x0, x1) = x1, [s](x0) = x0 + 1 orientation: g#(c(x,s(y))) = y + 1 >= y = g#(c(s(x),y)) f(c(s(x),y)) = 0 >= 0 = f(c(x,s(y))) g(c(x,s(y))) = 0 >= 0 = g(c(s(x),y)) g(s(f(x))) = 0 >= 0 = g(f(x)) problem: DPs: TRS: f(c(s(x),y)) -> f(c(x,s(y))) g(c(x,s(y))) -> g(c(s(x),y)) g(s(f(x))) -> g(f(x)) Qed