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