Consider the TRS R consisting of the rewrite rules

1: app(nil,YS) -> YS
2: app(cons(X),YS) -> cons(X)
3: from(X) -> cons(X)
4: zWadr(nil,YS) -> nil
5: zWadr(XS,nil) -> nil
6: zWadr(cons(X),cons(Y)) -> cons(app(Y,cons(X)))
7: prefix(L) -> cons(nil)

There is one dependency pair:

8: ZWADR(cons(X),cons(Y)) -> APP(Y,cons(X))

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.