YES

The TRS could be proven terminating. The proof took 18 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (2ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

zWadr^#(cons(X), cons(Y))

→

app^#(Y, cons(X))

Rewrite Rules

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)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, prefix, from, nil, cons

Strategy

There are no SCCs!