The rewrite relation of the following TRS is considered.
active(f(a,X,X)) | → | mark(f(X,b,b)) | (1) |
active(b) | → | mark(a) | (2) |
active(f(X1,X2,X3)) | → | f(X1,active(X2),X3) | (3) |
f(X1,mark(X2),X3) | → | mark(f(X1,X2,X3)) | (4) |
proper(f(X1,X2,X3)) | → | f(proper(X1),proper(X2),proper(X3)) | (5) |
proper(a) | → | ok(a) | (6) |
proper(b) | → | ok(b) | (7) |
f(ok(X1),ok(X2),ok(X3)) | → | ok(f(X1,X2,X3)) | (8) |
top(mark(X)) | → | top(proper(X)) | (9) |
top(ok(X)) | → | top(active(X)) | (10) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(f(a,X,X)) | → | mark(f(X,b,b)) | (1) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
top(ok(X)) | → | top(active(X)) | (10) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(b) | → | mark(a) | (2) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
top(mark(X)) | → | top(proper(X)) | (9) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(f(X1,X2,X3)) | → | f(X1,active(X2),X3) | (3) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
proper(f(X1,X2,X3)) | → | f(proper(X1),proper(X2),proper(X3)) | (5) |
prec(ok) | = | 0 | weight(ok) | = | 2 | ||||
prec(proper) | = | 2 | weight(proper) | = | 2 | ||||
prec(mark) | = | 1 | weight(mark) | = | 1 | ||||
prec(b) | = | 3 | weight(b) | = | 2 | ||||
prec(f) | = | 5 | weight(f) | = | 0 | ||||
prec(a) | = | 7 | weight(a) | = | 4 |
f(X1,mark(X2),X3) | → | mark(f(X1,X2,X3)) | (4) |
proper(a) | → | ok(a) | (6) |
proper(b) | → | ok(b) | (7) |
f(ok(X1),ok(X2),ok(X3)) | → | ok(f(X1,X2,X3)) | (8) |
There are no rules in the TRS. Hence, it is terminating.