The rewrite relation of the following TRS is considered.
active(f(f(X))) | → | mark(c(f(g(f(X))))) | (1) |
active(c(X)) | → | mark(d(X)) | (2) |
active(h(X)) | → | mark(c(d(X))) | (3) |
mark(f(X)) | → | active(f(mark(X))) | (4) |
mark(c(X)) | → | active(c(X)) | (5) |
mark(g(X)) | → | active(g(X)) | (6) |
mark(d(X)) | → | active(d(X)) | (7) |
mark(h(X)) | → | active(h(mark(X))) | (8) |
f(mark(X)) | → | f(X) | (9) |
f(active(X)) | → | f(X) | (10) |
c(mark(X)) | → | c(X) | (11) |
c(active(X)) | → | c(X) | (12) |
g(mark(X)) | → | g(X) | (13) |
g(active(X)) | → | g(X) | (14) |
d(mark(X)) | → | d(X) | (15) |
d(active(X)) | → | d(X) | (16) |
h(mark(X)) | → | h(X) | (17) |
h(active(X)) | → | h(X) | (18) |
f(f(active(X))) | → | f(g(f(c(mark(X))))) | (19) |
c(active(X)) | → | d(mark(X)) | (20) |
h(active(X)) | → | d(c(mark(X))) | (21) |
f(mark(X)) | → | mark(f(active(X))) | (22) |
c(mark(X)) | → | c(active(X)) | (23) |
g(mark(X)) | → | g(active(X)) | (24) |
d(mark(X)) | → | d(active(X)) | (25) |
h(mark(X)) | → | mark(h(active(X))) | (26) |
mark(f(X)) | → | f(X) | (27) |
active(f(X)) | → | f(X) | (28) |
mark(c(X)) | → | c(X) | (29) |
active(c(X)) | → | c(X) | (30) |
mark(g(X)) | → | g(X) | (31) |
active(g(X)) | → | g(X) | (32) |
mark(d(X)) | → | d(X) | (33) |
active(d(X)) | → | d(X) | (34) |
mark(h(X)) | → | h(X) | (35) |
active(h(X)) | → | h(X) | (36) |
[mark(x1)] | = | 0 · x1 + -∞ |
[active(x1)] | = | 0 · x1 + -∞ |
[c(x1)] | = | 0 · x1 + -∞ |
[d(x1)] | = | 0 · x1 + -∞ |
[f(x1)] | = | 0 · x1 + -∞ |
[h(x1)] | = | 2 · x1 + -∞ |
[g(x1)] | = | 0 · x1 + -∞ |
h(active(X)) | → | d(c(mark(X))) | (21) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[d(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[h(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
c(active(X)) | → | d(mark(X)) | (20) |
[mark(x1)] | = |
|
||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[d(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[h(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
f(mark(X)) | → | mark(f(active(X))) | (22) |
c(mark(X)) | → | c(active(X)) | (23) |
g(mark(X)) | → | g(active(X)) | (24) |
d(mark(X)) | → | d(active(X)) | (25) |
mark(f(X)) | → | f(X) | (27) |
mark(c(X)) | → | c(X) | (29) |
mark(g(X)) | → | g(X) | (31) |
mark(d(X)) | → | d(X) | (33) |
mark(h(X)) | → | h(X) | (35) |
f#(f(active(X))) | → | f#(c(mark(X))) | (37) |
f#(f(active(X))) | → | f#(g(f(c(mark(X))))) | (38) |
h#(mark(X)) | → | active#(X) | (39) |
h#(mark(X)) | → | h#(active(X)) | (40) |
The dependency pairs are split into 1 component.
h#(mark(X)) | → | h#(active(X)) | (40) |
π(h#) | = | { 1 } |
π(active) | = | { 1 } |
h#(mark(X)) | → | h#(active(X)) | (40) |
There are no pairs anymore.