CeTA: 1: error when switching from the TRS tail(cons(X)) -> L incr(nil) -> nil incr(cons(X)) -> cons(s(X)) adx(nil) -> nil adx(cons(X)) -> incr(cons(X)) nats -> adx(zeros) zeros -> cons(0) head(cons(X)) -> X to the initial DP problem dependency pairs: nats# -> zeros# nats# -> adx#(zeros) adx#(cons(X)) -> incr#(cons(X)) rewrite system: tail(cons(X)) -> L incr(nil) -> nil incr(cons(X)) -> cons(s(X)) adx(nil) -> nil adx(cons(X)) -> incr(cons(X)) nats -> adx(zeros) zeros -> cons(0) head(cons(X)) -> X the DP-transformation is not applied correctly. the TRS is not well-formed the variable L occurs only in the right-hand side of rule tail(cons(X)) -> L