The rewrite relation of the following TRS is considered.
sel(s(X),cons(Y,Z)) | → | sel(X,Z) | (1) |
sel(0,cons(X,Z)) | → | X | (2) |
first(0,Z) | → | nil | (3) |
first(s(X),cons(Y,Z)) | → | cons(Y,first(X,Z)) | (4) |
from(X) | → | cons(X,from(s(X))) | (5) |
sel1(s(X),cons(Y,Z)) | → | sel1(X,Z) | (6) |
sel1(0,cons(X,Z)) | → | quote(X) | (7) |
first1(0,Z) | → | nil1 | (8) |
first1(s(X),cons(Y,Z)) | → | cons1(quote(Y),first1(X,Z)) | (9) |
quote(0) | → | 01 | (10) |
quote1(cons(X,Z)) | → | cons1(quote(X),quote1(Z)) | (11) |
quote1(nil) | → | nil1 | (12) |
quote(s(X)) | → | s1(quote(X)) | (13) |
quote(sel(X,Z)) | → | sel1(X,Z) | (14) |
quote1(first(X,Z)) | → | first1(X,Z) | (15) |
unquote(01) | → | 0 | (16) |
unquote(s1(X)) | → | s(unquote(X)) | (17) |
unquote1(nil1) | → | nil | (18) |
unquote1(cons1(X,Z)) | → | fcons(unquote(X),unquote1(Z)) | (19) |
fcons(X,Z) | → | cons(X,Z) | (20) |
sel#(s(X),cons(Y,Z)) | → | sel#(X,Z) | (21) |
first#(s(X),cons(Y,Z)) | → | first#(X,Z) | (22) |
from#(X) | → | from#(s(X)) | (23) |
sel1#(s(X),cons(Y,Z)) | → | sel1#(X,Z) | (24) |
sel1#(0,cons(X,Z)) | → | quote#(X) | (25) |
first1#(s(X),cons(Y,Z)) | → | quote#(Y) | (26) |
first1#(s(X),cons(Y,Z)) | → | first1#(X,Z) | (27) |
quote1#(cons(X,Z)) | → | quote#(X) | (28) |
quote1#(cons(X,Z)) | → | quote1#(Z) | (29) |
quote#(s(X)) | → | quote#(X) | (30) |
quote#(sel(X,Z)) | → | sel1#(X,Z) | (31) |
quote1#(first(X,Z)) | → | first1#(X,Z) | (32) |
unquote#(s1(X)) | → | unquote#(X) | (33) |
unquote1#(cons1(X,Z)) | → | fcons#(unquote(X),unquote1(Z)) | (34) |
unquote1#(cons1(X,Z)) | → | unquote#(X) | (35) |
unquote1#(cons1(X,Z)) | → | unquote1#(Z) | (36) |
sel#(s(X),cons(Y,Z)) | → | sel#(X,Z) | (21) |
first#(s(X),cons(Y,Z)) | → | first#(X,Z) | (22) |
sel1#(s(X),cons(Y,Z)) | → | sel1#(X,Z) | (24) |
sel1#(0,cons(X,Z)) | → | quote#(X) | (25) |
first1#(s(X),cons(Y,Z)) | → | quote#(Y) | (26) |
first1#(s(X),cons(Y,Z)) | → | first1#(X,Z) | (27) |
quote1#(cons(X,Z)) | → | quote#(X) | (28) |
quote1#(cons(X,Z)) | → | quote1#(Z) | (29) |
quote#(s(X)) | → | quote#(X) | (30) |
quote#(sel(X,Z)) | → | sel1#(X,Z) | (31) |
quote1#(first(X,Z)) | → | first1#(X,Z) | (32) |
unquote#(s1(X)) | → | unquote#(X) | (33) |
unquote1#(cons1(X,Z)) | → | fcons#(unquote(X),unquote1(Z)) | (34) |
unquote1#(cons1(X,Z)) | → | unquote#(X) | (35) |
unquote1#(cons1(X,Z)) | → | unquote1#(Z) | (36) |
sel(s(x0),cons(x1,x2)) |
sel(0,cons(x0,x1)) |
first(0,x0) |
first(s(x0),cons(x1,x2)) |
from(x0) |
sel1(s(x0),cons(x1,x2)) |
sel1(0,cons(x0,x1)) |
first1(0,x0) |
first1(s(x0),cons(x1,x2)) |
quote(0) |
quote1(cons(x0,x1)) |
quote1(nil) |
quote(s(x0)) |
quote(sel(x0,x1)) |
quote1(first(x0,x1)) |
unquote(01) |
unquote(s1(x0)) |
unquote1(nil1) |
unquote1(cons1(x0,x1)) |
fcons(x0,x1) |
sel(s(X),cons(Y,Z)) | → | sel(X,Z) | (1) |
sel(0,cons(X,Z)) | → | X | (2) |
first(0,Z) | → | nil | (3) |
first(s(X),cons(Y,Z)) | → | cons(Y,first(X,Z)) | (4) |
from(X) | → | cons(X,from(s(X))) | (5) |
sel1(s(X),cons(Y,Z)) | → | sel1(X,Z) | (6) |
sel1(0,cons(X,Z)) | → | quote(X) | (7) |
first1(0,Z) | → | nil1 | (8) |
first1(s(X),cons(Y,Z)) | → | cons1(quote(Y),first1(X,Z)) | (9) |
quote(0) | → | 01 | (10) |
quote1(cons(X,Z)) | → | cons1(quote(X),quote1(Z)) | (11) |
quote1(nil) | → | nil1 | (12) |
quote(s(X)) | → | s1(quote(X)) | (13) |
quote(sel(X,Z)) | → | sel1(X,Z) | (14) |
quote1(first(X,Z)) | → | first1(X,Z) | (15) |
unquote(01) | → | 0 | (16) |
unquote(s1(X)) | → | s(unquote(X)) | (17) |
unquote1(nil1) | → | nil | (18) |
unquote1(cons1(X,Z)) | → | fcons(unquote(X),unquote1(Z)) | (19) |
fcons(X,Z) | → | cons(X,Z) | (20) |
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
from#(s(z0)) | → | from#(s(s(z0))) | (37) |
from#(s(s(z0))) | → | from#(s(s(s(z0)))) | (38) |
t0 | = | from#(s(s(z0))) |
→P | from#(s(s(s(z0)))) | |
= | t1 |