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