The rewrite relation of the following TRS is considered.
app(nil,YS) | → | YS | (1) |
app(cons(X),YS) | → | cons(X) | (2) |
from(X) | → | cons(X) | (3) |
zWadr(nil,YS) | → | nil | (4) |
zWadr(XS,nil) | → | nil | (5) |
zWadr(cons(X),cons(Y)) | → | cons(app(Y,cons(X))) | (6) |
prefix(L) | → | cons(nil) | (7) |
zWadr#(cons(X),cons(Y)) | → | app#(Y,cons(X)) | (8) |
The dependency pairs are split into 0 components.