YES Problem: f(c(X,s(Y))) -> f(c(s(X),Y)) g(c(s(X),Y)) -> f(c(X,s(Y))) Proof: DP Processor: DPs: f#(c(X,s(Y))) -> f#(c(s(X),Y)) g#(c(s(X),Y)) -> f#(c(X,s(Y))) TRS: f(c(X,s(Y))) -> f(c(s(X),Y)) g(c(s(X),Y)) -> f(c(X,s(Y))) Usable Rule Processor: DPs: f#(c(X,s(Y))) -> f#(c(s(X),Y)) g#(c(s(X),Y)) -> f#(c(X,s(Y))) TRS: ADG Processor: DPs: f#(c(X,s(Y))) -> f#(c(s(X),Y)) g#(c(s(X),Y)) -> f#(c(X,s(Y))) TRS: graph: g#(c(s(X),Y)) -> f#(c(X,s(Y))) -> f#(c(X,s(Y))) -> f#(c(s(X),Y)) f#(c(X,s(Y))) -> f#(c(s(X),Y)) -> f#(c(X,s(Y))) -> f#(c(s(X),Y)) Restore Modifier: DPs: f#(c(X,s(Y))) -> f#(c(s(X),Y)) g#(c(s(X),Y)) -> f#(c(X,s(Y))) TRS: f(c(X,s(Y))) -> f(c(s(X),Y)) g(c(s(X),Y)) -> f(c(X,s(Y))) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: f#(c(X,s(Y))) -> f#(c(s(X),Y)) TRS: f(c(X,s(Y))) -> f(c(s(X),Y)) g(c(s(X),Y)) -> f(c(X,s(Y))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0) = x0, [g](x0) = 0, [f](x0) = 0, [c](x0, x1) = x1, [s](x0) = x0 + 1 orientation: f#(c(X,s(Y))) = Y + 1 >= Y = f#(c(s(X),Y)) f(c(X,s(Y))) = 0 >= 0 = f(c(s(X),Y)) g(c(s(X),Y)) = 0 >= 0 = f(c(X,s(Y))) problem: DPs: TRS: f(c(X,s(Y))) -> f(c(s(X),Y)) g(c(s(X),Y)) -> f(c(X,s(Y))) Qed