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