The rewrite relation of the following TRS is considered.
sel(s(X),cons(Y)) | → | sel(X,Z) | (1) |
sel1(s(X),cons(Y)) | → | sel1(X,Z) | (2) |
first1(s(X),cons(Y)) | → | cons1(quote,first1(X,Z)) | (3) |
quote | → | sel1(X,Z) | (4) |
quote1 | → | first1(X,Z) | (5) |
sel(0,cons(X)) | → | X | (6) |
first(0,Z) | → | nil | (7) |
first(s(X),cons(Y)) | → | cons(Y) | (8) |
from(X) | → | cons(X) | (9) |
sel1(0,cons(X)) | → | quote | (10) |
first1(0,Z) | → | nil1 | (11) |
quote | → | 01 | (12) |
quote1 | → | cons1(quote,quote1) | (13) |
quote1 | → | nil1 | (14) |
quote | → | s1(quote) | (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) | (20) |
t0 | = | sel(s(X),cons(Y)) |
→ | sel(X,sel(s(X),cons(Y))) | |
= | t1 |