CeTA: 1: error when switching from the TRS tail(cons(X)) -> XS pairNs -> cons(0) oddNs -> incr(pairNs) incr(cons(X)) -> cons(s(X)) take(0,XS) -> nil take(s(N),cons(X)) -> cons(X) zip(nil,XS) -> nil zip(X,nil) -> nil zip(cons(X),cons(Y)) -> cons(pair(X,Y)) repItems(nil) -> nil repItems(cons(X)) -> cons(X) to the initial DP problem dependency pairs: oddNs# -> incr#(pairNs) oddNs# -> pairNs# rewrite system: tail(cons(X)) -> XS pairNs -> cons(0) oddNs -> incr(pairNs) incr(cons(X)) -> cons(s(X)) take(0,XS) -> nil take(s(N),cons(X)) -> cons(X) zip(nil,XS) -> nil zip(X,nil) -> nil zip(cons(X),cons(Y)) -> cons(pair(X,Y)) repItems(nil) -> nil repItems(cons(X)) -> cons(X) the DP-transformation is not applied correctly. the TRS is not well-formed the variable XS occurs only in the right-hand side of rule tail(cons(X)) -> XS