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) |
[active(x1)] | = | 1 · x1 + 1 |
[c] | = | 0 |
[mark(x1)] | = | 1 · x1 + 1 |
[f(x1)] | = | 1 · x1 |
[g(x1)] | = | 1 · x1 |
f(mark(X)) | → | f(X) | (6) |
f(active(X)) | → | f(X) | (7) |
g(mark(X)) | → | g(X) | (8) |
g(active(X)) | → | g(X) | (9) |
The TRS is overlay and locally confluent:
10Hence, it suffices to show innermost termination in the following.
active#(c) | → | mark#(f(g(c))) | (10) |
active#(f(g(X))) | → | mark#(g(X)) | (11) |
mark#(c) | → | active#(c) | (12) |
mark#(f(X)) | → | active#(f(X)) | (13) |
mark#(g(X)) | → | active#(g(X)) | (14) |
The dependency pairs are split into 0 components.