The rewrite relation of the following TRS is considered.
active(2nd(cons(X,cons(Y,Z)))) | → | mark(Y) | (1) |
active(from(X)) | → | mark(cons(X,from(s(X)))) | (2) |
mark(2nd(X)) | → | active(2nd(mark(X))) | (3) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (4) |
mark(from(X)) | → | active(from(mark(X))) | (5) |
mark(s(X)) | → | active(s(mark(X))) | (6) |
2nd(mark(X)) | → | 2nd(X) | (7) |
2nd(active(X)) | → | 2nd(X) | (8) |
cons(mark(X1),X2) | → | cons(X1,X2) | (9) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (10) |
cons(active(X1),X2) | → | cons(X1,X2) | (11) |
cons(X1,active(X2)) | → | cons(X1,X2) | (12) |
from(mark(X)) | → | from(X) | (13) |
from(active(X)) | → | from(X) | (14) |
s(mark(X)) | → | s(X) | (15) |
s(active(X)) | → | s(X) | (16) |
[from(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[2nd(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(2nd(cons(X,cons(Y,Z)))) | → | mark(Y) | (1) |
[from(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[2nd(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(from(X)) | → | mark(cons(X,from(s(X)))) | (2) |
[from(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[2nd(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
mark(from(X)) | → | active(from(mark(X))) | (5) |
[from(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[2nd(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
2nd(mark(X)) | → | 2nd(X) | (7) |
cons(mark(X1),X2) | → | cons(X1,X2) | (9) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (10) |
from(mark(X)) | → | from(X) | (13) |
s(mark(X)) | → | s(X) | (15) |
[from(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[2nd(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
mark(2nd(X)) | → | active(2nd(mark(X))) | (3) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (4) |
mark(s(X)) | → | active(s(mark(X))) | (6) |
prec(s) | = | 1 | weight(s) | = | 2 | ||||
prec(from) | = | 2 | weight(from) | = | 2 | ||||
prec(active) | = | 0 | weight(active) | = | 2 | ||||
prec(2nd) | = | 5 | weight(2nd) | = | 2 | ||||
prec(cons) | = | 4 | weight(cons) | = | 0 |
2nd(active(X)) | → | 2nd(X) | (8) |
cons(active(X1),X2) | → | cons(X1,X2) | (11) |
cons(X1,active(X2)) | → | cons(X1,X2) | (12) |
from(active(X)) | → | from(X) | (14) |
s(active(X)) | → | s(X) | (16) |
There are no rules in the TRS. Hence, it is terminating.