The rewrite relation of the following TRS is considered.
active(c) | → | mark(f(g(c))) | (1) |
active(f(g(X))) | → | mark(g(X)) | (2) |
mark(c) | → | active(c) | (3) |
mark(f(X)) | → | active(f(X)) | (4) |
mark(g(X)) | → | active(g(X)) | (5) |
f(mark(X)) | → | f(X) | (6) |
f(active(X)) | → | f(X) | (7) |
g(mark(X)) | → | g(X) | (8) |
g(active(X)) | → | g(X) | (9) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
f(mark(X)) | → | f(X) | (6) |
f(active(X)) | → | f(X) | (7) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
g(active(X)) | → | g(X) | (9) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
g(mark(X)) | → | g(X) | (8) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
active(f(g(X))) | → | mark(g(X)) | (2) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
mark(g(X)) | → | active(g(X)) | (5) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
mark(f(X)) | → | active(f(X)) | (4) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[c] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[g(x1)] | = |
|
active(c) | → | mark(f(g(c))) | (1) |
prec(mark) | = | 0 | status(mark) | = | [1] | list-extension(mark) | = | Lex | ||
prec(active) | = | 0 | status(active) | = | [1] | list-extension(active) | = | Lex | ||
prec(c) | = | 0 | status(c) | = | [] | list-extension(c) | = | Lex |
[mark(x1)] | = | max(1, 2 + 1 · x1) |
[active(x1)] | = | max(0, 1 + 1 · x1) |
[c] | = | max(1) |
mark(c) | → | active(c) | (3) |
There are no rules in the TRS. Hence, it is terminating.