The rewrite relation of the following TRS is considered.
app(nil,YS) | → | YS | (1) |
app(cons(X,XS),YS) | → | cons(X,app(XS,YS)) | (2) |
from(X) | → | cons(X,from(s(X))) | (3) |
zWadr(nil,YS) | → | nil | (4) |
zWadr(XS,nil) | → | nil | (5) |
zWadr(cons(X,XS),cons(Y,YS)) | → | cons(app(Y,cons(X,nil)),zWadr(XS,YS)) | (6) |
prefix(L) | → | cons(nil,zWadr(L,prefix(L))) | (7) |
t0 | = | from(X) |
→ | cons(X,from(s(X))) | |
= | t1 |