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())} POP*: Precedence: zWadr > app, zWadr > cons, from > cons, prefix > cons, prefix > nil empty Normal: pi(prefix) = [1], pi(zWadr) = [1,2], pi(from) = [1], pi(app) = [1,2] Safe: pi(cons) = [1] Predicative System: { 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())} Qed