The rewrite relation of the following TRS is considered.
active(f(a,b,X)) | → | mark(f(X,X,X)) | (1) |
active(c) | → | mark(a) | (2) |
active(c) | → | mark(b) | (3) |
mark(f(X1,X2,X3)) | → | active(f(X1,X2,mark(X3))) | (4) |
mark(a) | → | active(a) | (5) |
mark(b) | → | active(b) | (6) |
mark(c) | → | active(c) | (7) |
f(mark(X1),X2,X3) | → | f(X1,X2,X3) | (8) |
f(X1,mark(X2),X3) | → | f(X1,X2,X3) | (9) |
f(X1,X2,mark(X3)) | → | f(X1,X2,X3) | (10) |
f(active(X1),X2,X3) | → | f(X1,X2,X3) | (11) |
f(X1,active(X2),X3) | → | f(X1,X2,X3) | (12) |
f(X1,X2,active(X3)) | → | f(X1,X2,X3) | (13) |
active#(f(a,b,X)) | → | mark#(f(X,X,X)) | (14) |
active#(f(a,b,X)) | → | f#(X,X,X) | (15) |
active#(c) | → | mark#(a) | (16) |
active#(c) | → | mark#(b) | (17) |
mark#(f(X1,X2,X3)) | → | active#(f(X1,X2,mark(X3))) | (18) |
mark#(f(X1,X2,X3)) | → | f#(X1,X2,mark(X3)) | (19) |
mark#(f(X1,X2,X3)) | → | mark#(X3) | (20) |
mark#(a) | → | active#(a) | (21) |
mark#(b) | → | active#(b) | (22) |
mark#(c) | → | active#(c) | (23) |
f#(mark(X1),X2,X3) | → | f#(X1,X2,X3) | (24) |
f#(X1,mark(X2),X3) | → | f#(X1,X2,X3) | (25) |
f#(X1,X2,mark(X3)) | → | f#(X1,X2,X3) | (26) |
f#(active(X1),X2,X3) | → | f#(X1,X2,X3) | (27) |
f#(X1,active(X2),X3) | → | f#(X1,X2,X3) | (28) |
f#(X1,X2,active(X3)) | → | f#(X1,X2,X3) | (29) |
The dependency pairs are split into 2 components.
mark#(f(X1,X2,X3)) | → | active#(f(X1,X2,mark(X3))) | (18) |
active#(f(a,b,X)) | → | mark#(f(X,X,X)) | (14) |
mark#(f(X1,X2,X3)) | → | mark#(X3) | (20) |
prec(f) | = | 3 | weight(f) | = | 1 | ||||
prec(a) | = | 0 | weight(a) | = | 1 | ||||
prec(b) | = | 1 | weight(b) | = | 2 | ||||
prec(c) | = | 2 | weight(c) | = | 3 |
π(mark#) | = | 1 |
π(f) | = | [3] |
π(active#) | = | 1 |
π(mark) | = | 1 |
π(active) | = | 1 |
π(a) | = | [] |
π(b) | = | [] |
π(c) | = | [] |
mark#(f(X1,X2,X3)) | → | mark#(X3) | (20) |
mark#(f(z0,z0,z0)) | → | active#(f(z0,z0,mark(z0))) | (30) |
mark#(f(x0,x0,x0)) | → | active#(f(x0,x0,x0)) | (31) |
mark#(f(f(x0,x1,x2),f(x0,x1,x2),f(x0,x1,x2))) | → | active#(f(f(x0,x1,x2),f(x0,x1,x2),active(f(x0,x1,mark(x2))))) | (32) |
mark#(f(a,a,a)) | → | active#(f(a,a,active(a))) | (33) |
mark#(f(b,b,b)) | → | active#(f(b,b,active(b))) | (34) |
mark#(f(c,c,c)) | → | active#(f(c,c,active(c))) | (35) |
The dependency pairs are split into 1 component.
mark#(f(f(x0,x1,x2),f(x0,x1,x2),f(x0,x1,x2))) | → | active#(f(f(x0,x1,x2),f(x0,x1,x2),active(f(x0,x1,mark(x2))))) | (32) |
active#(f(a,b,X)) | → | mark#(f(X,X,X)) | (14) |
mark#(f(a,a,a)) | → | active#(f(a,a,active(a))) | (33) |
mark#(f(b,b,b)) | → | active#(f(b,b,active(b))) | (34) |
mark#(f(c,c,c)) | → | active#(f(c,c,active(c))) | (35) |
active#(f(a,b,f(y_0,y_1,y_2))) | → | mark#(f(f(y_0,y_1,y_2),f(y_0,y_1,y_2),f(y_0,y_1,y_2))) | (36) |
active#(f(a,b,a)) | → | mark#(f(a,a,a)) | (37) |
active#(f(a,b,b)) | → | mark#(f(b,b,b)) | (38) |
active#(f(a,b,c)) | → | mark#(f(c,c,c)) | (39) |
[mark#(x1)] | = |
|
||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||
[active#(x1)] | = |
|
||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||
[a] | = |
|
||||||||||||||||
[b] | = |
|
||||||||||||||||
[c] | = |
|
active#(f(a,b,b)) | → | mark#(f(b,b,b)) | (38) |
The dependency pairs are split into 1 component.
active#(f(a,b,f(y_0,y_1,y_2))) | → | mark#(f(f(y_0,y_1,y_2),f(y_0,y_1,y_2),f(y_0,y_1,y_2))) | (36) |
mark#(f(f(x0,x1,x2),f(x0,x1,x2),f(x0,x1,x2))) | → | active#(f(f(x0,x1,x2),f(x0,x1,x2),active(f(x0,x1,mark(x2))))) | (32) |
active#(f(a,b,a)) | → | mark#(f(a,a,a)) | (37) |
mark#(f(a,a,a)) | → | active#(f(a,a,active(a))) | (33) |
active#(f(a,b,c)) | → | mark#(f(c,c,c)) | (39) |
mark#(f(c,c,c)) | → | active#(f(c,c,active(c))) | (35) |
[active#(x1)] | = |
|
||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||
[a] | = |
|
||||||||||||||||
[b] | = |
|
||||||||||||||||
[mark#(x1)] | = |
|
||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||
[c] | = |
|
active#(f(a,b,a)) | → | mark#(f(a,a,a)) | (37) |
The dependency pairs are split into 1 component.
mark#(f(f(x0,x1,x2),f(x0,x1,x2),f(x0,x1,x2))) | → | active#(f(f(x0,x1,x2),f(x0,x1,x2),active(f(x0,x1,mark(x2))))) | (32) |
active#(f(a,b,f(y_0,y_1,y_2))) | → | mark#(f(f(y_0,y_1,y_2),f(y_0,y_1,y_2),f(y_0,y_1,y_2))) | (36) |
active#(f(a,b,c)) | → | mark#(f(c,c,c)) | (39) |
mark#(f(c,c,c)) | → | active#(f(c,c,active(c))) | (35) |
[mark#(x1)] | = |
|
||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[active#(x1)] | = |
|
||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||
[c] | = |
|
f(X1,mark(X2),X3) | → | f(X1,X2,X3) | (9) |
f(mark(X1),X2,X3) | → | f(X1,X2,X3) | (8) |
f(X1,X2,mark(X3)) | → | f(X1,X2,X3) | (10) |
f(active(X1),X2,X3) | → | f(X1,X2,X3) | (11) |
f(X1,active(X2),X3) | → | f(X1,X2,X3) | (12) |
f(X1,X2,active(X3)) | → | f(X1,X2,X3) | (13) |
mark#(f(c,c,c)) | → | active#(f(c,c,active(c))) | (35) |
The dependency pairs are split into 1 component.
active#(f(a,b,f(y_0,y_1,y_2))) | → | mark#(f(f(y_0,y_1,y_2),f(y_0,y_1,y_2),f(y_0,y_1,y_2))) | (36) |
mark#(f(f(x0,x1,x2),f(x0,x1,x2),f(x0,x1,x2))) | → | active#(f(f(x0,x1,x2),f(x0,x1,x2),active(f(x0,x1,mark(x2))))) | (32) |
[active#(x1)] | = |
|
||||||||||||||||||||||||||
[f(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||
[b] | = |
|
||||||||||||||||||||||||||
[mark#(x1)] | = |
|
||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||
[c] | = |
|
f(X1,mark(X2),X3) | → | f(X1,X2,X3) | (9) |
f(mark(X1),X2,X3) | → | f(X1,X2,X3) | (8) |
f(X1,X2,mark(X3)) | → | f(X1,X2,X3) | (10) |
f(active(X1),X2,X3) | → | f(X1,X2,X3) | (11) |
f(X1,active(X2),X3) | → | f(X1,X2,X3) | (12) |
f(X1,X2,active(X3)) | → | f(X1,X2,X3) | (13) |
active#(f(a,b,f(y_0,y_1,y_2))) | → | mark#(f(f(y_0,y_1,y_2),f(y_0,y_1,y_2),f(y_0,y_1,y_2))) | (36) |
There are no rules.
There are no pairs anymore.
f#(X1,mark(X2),X3) | → | f#(X1,X2,X3) | (25) |
f#(mark(X1),X2,X3) | → | f#(X1,X2,X3) | (24) |
f#(X1,X2,mark(X3)) | → | f#(X1,X2,X3) | (26) |
f#(active(X1),X2,X3) | → | f#(X1,X2,X3) | (27) |
f#(X1,active(X2),X3) | → | f#(X1,X2,X3) | (28) |
f#(X1,X2,active(X3)) | → | f#(X1,X2,X3) | (29) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(f(a,b,x0)) |
active(c) |
mark(f(x0,x1,x2)) |
mark(a) |
mark(b) |
mark(c) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
f#(X1,mark(X2),X3) | → | f#(X1,X2,X3) | (25) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
f#(mark(X1),X2,X3) | → | f#(X1,X2,X3) | (24) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
f#(X1,X2,mark(X3)) | → | f#(X1,X2,X3) | (26) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 | |
f#(active(X1),X2,X3) | → | f#(X1,X2,X3) | (27) |
1 | > | 1 | |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
f#(X1,active(X2),X3) | → | f#(X1,X2,X3) | (28) |
1 | ≥ | 1 | |
2 | > | 2 | |
3 | ≥ | 3 | |
f#(X1,X2,active(X3)) | → | f#(X1,X2,X3) | (29) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 |
As there is no critical graph in the transitive closure, there are no infinite chains.