TRS: { app(nil(), YS) -> YS, app(cons(X), YS) -> cons(X), from(X) -> cons(X), zWadr(nil(), YS) -> nil(), zWadr(XS, nil()) -> nil(), zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X))), prefix(L) -> cons(nil())} MPO: Prec: zWadr > app, zWadr > cons, from > cons, prefix > cons, prefix > nil empty Strict: {} Weak: {} Qed