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) |
app(nil,x0) |
app(cons(x0,x1),x2) |
from(x0) |
zWadr(nil,x0) |
zWadr(x0,nil) |
zWadr(cons(x0,x1),cons(x2,x3)) |
prefix(x0) |
app#(cons(X,XS),YS) | → | app#(XS,YS) | (8) |
from#(X) | → | from#(s(X)) | (9) |
zWadr#(cons(X,XS),cons(Y,YS)) | → | app#(Y,cons(X,nil)) | (10) |
zWadr#(cons(X,XS),cons(Y,YS)) | → | zWadr#(XS,YS) | (11) |
prefix#(L) | → | zWadr#(L,prefix(L)) | (12) |
prefix#(L) | → | prefix#(L) | (13) |
app#(cons(X,XS),YS) | → | app#(XS,YS) | (8) |
zWadr#(cons(X,XS),cons(Y,YS)) | → | app#(Y,cons(X,nil)) | (10) |
zWadr#(cons(X,XS),cons(Y,YS)) | → | zWadr#(XS,YS) | (11) |
prefix#(L) | → | zWadr#(L,prefix(L)) | (12) |
prefix#(L) | → | prefix#(L) | (13) |
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) |
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
from#(s(z0)) | → | from#(s(s(z0))) | (14) |
from#(s(s(z0))) | → | from#(s(s(s(z0)))) | (15) |
t0 | = | from#(s(s(z0))) |
→P | from#(s(s(s(z0)))) | |
= | t1 |