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))) TDG 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))) 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)) 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))) CDG Processor: 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))) graph: Qed