Term Rewriting System R:
[YS, X, XS, Y, L]
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)

Innermost Termination of R to be shown.

Dependency Pair Analysis

R contains the following Dependency Pairs:

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

R contains no SCCs.

Innermost Termination of R successfully shown.
0:00 minutes