The rewrite relation of the following TRS is considered.
active(eq(0,0)) | → | mark(true) | (1) |
active(eq(s(X),s(Y))) | → | mark(eq(X,Y)) | (2) |
active(eq(X,Y)) | → | mark(false) | (3) |
active(inf(X)) | → | mark(cons(X,inf(s(X)))) | (4) |
active(take(0,X)) | → | mark(nil) | (5) |
active(take(s(X),cons(Y,L))) | → | mark(cons(Y,take(X,L))) | (6) |
active(length(nil)) | → | mark(0) | (7) |
active(length(cons(X,L))) | → | mark(s(length(L))) | (8) |
mark(eq(X1,X2)) | → | active(eq(X1,X2)) | (9) |
mark(0) | → | active(0) | (10) |
mark(true) | → | active(true) | (11) |
mark(s(X)) | → | active(s(X)) | (12) |
mark(false) | → | active(false) | (13) |
mark(inf(X)) | → | active(inf(mark(X))) | (14) |
mark(cons(X1,X2)) | → | active(cons(X1,X2)) | (15) |
mark(take(X1,X2)) | → | active(take(mark(X1),mark(X2))) | (16) |
mark(nil) | → | active(nil) | (17) |
mark(length(X)) | → | active(length(mark(X))) | (18) |
eq(mark(X1),X2) | → | eq(X1,X2) | (19) |
eq(X1,mark(X2)) | → | eq(X1,X2) | (20) |
eq(active(X1),X2) | → | eq(X1,X2) | (21) |
eq(X1,active(X2)) | → | eq(X1,X2) | (22) |
s(mark(X)) | → | s(X) | (23) |
s(active(X)) | → | s(X) | (24) |
inf(mark(X)) | → | inf(X) | (25) |
inf(active(X)) | → | inf(X) | (26) |
cons(mark(X1),X2) | → | cons(X1,X2) | (27) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (28) |
cons(active(X1),X2) | → | cons(X1,X2) | (29) |
cons(X1,active(X2)) | → | cons(X1,X2) | (30) |
take(mark(X1),X2) | → | take(X1,X2) | (31) |
take(X1,mark(X2)) | → | take(X1,X2) | (32) |
take(active(X1),X2) | → | take(X1,X2) | (33) |
take(X1,active(X2)) | → | take(X1,X2) | (34) |
length(mark(X)) | → | length(X) | (35) |
length(active(X)) | → | length(X) | (36) |
active#(eq(0,0)) | → | mark#(true) | (37) |
active#(eq(s(X),s(Y))) | → | mark#(eq(X,Y)) | (38) |
active#(eq(s(X),s(Y))) | → | eq#(X,Y) | (39) |
active#(eq(X,Y)) | → | mark#(false) | (40) |
active#(inf(X)) | → | mark#(cons(X,inf(s(X)))) | (41) |
active#(inf(X)) | → | cons#(X,inf(s(X))) | (42) |
active#(inf(X)) | → | inf#(s(X)) | (43) |
active#(inf(X)) | → | s#(X) | (44) |
active#(take(0,X)) | → | mark#(nil) | (45) |
active#(take(s(X),cons(Y,L))) | → | mark#(cons(Y,take(X,L))) | (46) |
active#(take(s(X),cons(Y,L))) | → | cons#(Y,take(X,L)) | (47) |
active#(take(s(X),cons(Y,L))) | → | take#(X,L) | (48) |
active#(length(nil)) | → | mark#(0) | (49) |
active#(length(cons(X,L))) | → | mark#(s(length(L))) | (50) |
active#(length(cons(X,L))) | → | s#(length(L)) | (51) |
active#(length(cons(X,L))) | → | length#(L) | (52) |
mark#(eq(X1,X2)) | → | active#(eq(X1,X2)) | (53) |
mark#(0) | → | active#(0) | (54) |
mark#(true) | → | active#(true) | (55) |
mark#(s(X)) | → | active#(s(X)) | (56) |
mark#(false) | → | active#(false) | (57) |
mark#(inf(X)) | → | active#(inf(mark(X))) | (58) |
mark#(inf(X)) | → | inf#(mark(X)) | (59) |
mark#(inf(X)) | → | mark#(X) | (60) |
mark#(cons(X1,X2)) | → | active#(cons(X1,X2)) | (61) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (62) |
mark#(take(X1,X2)) | → | take#(mark(X1),mark(X2)) | (63) |
mark#(take(X1,X2)) | → | mark#(X1) | (64) |
mark#(take(X1,X2)) | → | mark#(X2) | (65) |
mark#(nil) | → | active#(nil) | (66) |
mark#(length(X)) | → | active#(length(mark(X))) | (67) |
mark#(length(X)) | → | length#(mark(X)) | (68) |
mark#(length(X)) | → | mark#(X) | (69) |
eq#(mark(X1),X2) | → | eq#(X1,X2) | (70) |
eq#(X1,mark(X2)) | → | eq#(X1,X2) | (71) |
eq#(active(X1),X2) | → | eq#(X1,X2) | (72) |
eq#(X1,active(X2)) | → | eq#(X1,X2) | (73) |
s#(mark(X)) | → | s#(X) | (74) |
s#(active(X)) | → | s#(X) | (75) |
inf#(mark(X)) | → | inf#(X) | (76) |
inf#(active(X)) | → | inf#(X) | (77) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (78) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (79) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (80) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (81) |
take#(mark(X1),X2) | → | take#(X1,X2) | (82) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (83) |
take#(active(X1),X2) | → | take#(X1,X2) | (84) |
take#(X1,active(X2)) | → | take#(X1,X2) | (85) |
length#(mark(X)) | → | length#(X) | (86) |
length#(active(X)) | → | length#(X) | (87) |
The dependency pairs are split into 8 components.
mark#(take(X1,X2)) | → | mark#(X1) | (64) |
mark#(inf(X)) | → | mark#(X) | (60) |
mark#(take(X1,X2)) | → | mark#(X2) | (65) |
mark#(length(X)) | → | mark#(X) | (69) |
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.
inf(mark(x0)) |
inf(active(x0)) |
take(mark(x0),x1) |
take(x0,mark(x1)) |
take(active(x0),x1) |
take(x0,active(x1)) |
length(mark(x0)) |
length(active(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
mark#(take(X1,X2)) | → | mark#(X1) | (64) |
1 | > | 1 | |
mark#(inf(X)) | → | mark#(X) | (60) |
1 | > | 1 | |
mark#(take(X1,X2)) | → | mark#(X2) | (65) |
1 | > | 1 | |
mark#(length(X)) | → | mark#(X) | (69) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
active#(eq(s(X),s(Y))) | → | mark#(eq(X,Y)) | (38) |
mark#(eq(X1,X2)) | → | active#(eq(X1,X2)) | (53) |
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.
eq(mark(x0),x1) |
eq(x0,mark(x1)) |
eq(active(x0),x1) |
eq(x0,active(x1)) |
s(mark(x0)) |
s(active(x0)) |
[active#(x1)] | = | 1 · x1 |
[eq(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[s(x1)] | = | 2 + 2 · x1 |
[mark#(x1)] | = | 2 · x1 |
active#(eq(s(X),s(Y))) | → | mark#(eq(X,Y)) | (38) |
mark#(eq(X1,X2)) | → | active#(eq(X1,X2)) | (53) |
There are no pairs anymore.
eq#(X1,mark(X2)) | → | eq#(X1,X2) | (71) |
eq#(mark(X1),X2) | → | eq#(X1,X2) | (70) |
eq#(active(X1),X2) | → | eq#(X1,X2) | (72) |
eq#(X1,active(X2)) | → | eq#(X1,X2) | (73) |
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(eq(x0,x1)) |
active(inf(x0)) |
active(take(0,x0)) |
active(take(s(x0),cons(x1,x2))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(eq(x0,x1)) |
mark(0) |
mark(true) |
mark(s(x0)) |
mark(false) |
mark(inf(x0)) |
mark(cons(x0,x1)) |
mark(take(x0,x1)) |
mark(nil) |
mark(length(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
eq#(X1,mark(X2)) | → | eq#(X1,X2) | (71) |
1 | ≥ | 1 | |
2 | > | 2 | |
eq#(mark(X1),X2) | → | eq#(X1,X2) | (70) |
1 | > | 1 | |
2 | ≥ | 2 | |
eq#(active(X1),X2) | → | eq#(X1,X2) | (72) |
1 | > | 1 | |
2 | ≥ | 2 | |
eq#(X1,active(X2)) | → | eq#(X1,X2) | (73) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
s#(active(X)) | → | s#(X) | (75) |
s#(mark(X)) | → | s#(X) | (74) |
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(eq(x0,x1)) |
active(inf(x0)) |
active(take(0,x0)) |
active(take(s(x0),cons(x1,x2))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(eq(x0,x1)) |
mark(0) |
mark(true) |
mark(s(x0)) |
mark(false) |
mark(inf(x0)) |
mark(cons(x0,x1)) |
mark(take(x0,x1)) |
mark(nil) |
mark(length(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
s#(active(X)) | → | s#(X) | (75) |
1 | > | 1 | |
s#(mark(X)) | → | s#(X) | (74) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
inf#(active(X)) | → | inf#(X) | (77) |
inf#(mark(X)) | → | inf#(X) | (76) |
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(eq(x0,x1)) |
active(inf(x0)) |
active(take(0,x0)) |
active(take(s(x0),cons(x1,x2))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(eq(x0,x1)) |
mark(0) |
mark(true) |
mark(s(x0)) |
mark(false) |
mark(inf(x0)) |
mark(cons(x0,x1)) |
mark(take(x0,x1)) |
mark(nil) |
mark(length(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
inf#(active(X)) | → | inf#(X) | (77) |
1 | > | 1 | |
inf#(mark(X)) | → | inf#(X) | (76) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (79) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (78) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (80) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (81) |
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(eq(x0,x1)) |
active(inf(x0)) |
active(take(0,x0)) |
active(take(s(x0),cons(x1,x2))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(eq(x0,x1)) |
mark(0) |
mark(true) |
mark(s(x0)) |
mark(false) |
mark(inf(x0)) |
mark(cons(x0,x1)) |
mark(take(x0,x1)) |
mark(nil) |
mark(length(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (79) |
1 | ≥ | 1 | |
2 | > | 2 | |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (78) |
1 | > | 1 | |
2 | ≥ | 2 | |
cons#(active(X1),X2) | → | cons#(X1,X2) | (80) |
1 | > | 1 | |
2 | ≥ | 2 | |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (81) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
take#(X1,mark(X2)) | → | take#(X1,X2) | (83) |
take#(mark(X1),X2) | → | take#(X1,X2) | (82) |
take#(active(X1),X2) | → | take#(X1,X2) | (84) |
take#(X1,active(X2)) | → | take#(X1,X2) | (85) |
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(eq(x0,x1)) |
active(inf(x0)) |
active(take(0,x0)) |
active(take(s(x0),cons(x1,x2))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(eq(x0,x1)) |
mark(0) |
mark(true) |
mark(s(x0)) |
mark(false) |
mark(inf(x0)) |
mark(cons(x0,x1)) |
mark(take(x0,x1)) |
mark(nil) |
mark(length(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
take#(X1,mark(X2)) | → | take#(X1,X2) | (83) |
1 | ≥ | 1 | |
2 | > | 2 | |
take#(mark(X1),X2) | → | take#(X1,X2) | (82) |
1 | > | 1 | |
2 | ≥ | 2 | |
take#(active(X1),X2) | → | take#(X1,X2) | (84) |
1 | > | 1 | |
2 | ≥ | 2 | |
take#(X1,active(X2)) | → | take#(X1,X2) | (85) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
length#(active(X)) | → | length#(X) | (87) |
length#(mark(X)) | → | length#(X) | (86) |
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(eq(x0,x1)) |
active(inf(x0)) |
active(take(0,x0)) |
active(take(s(x0),cons(x1,x2))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(eq(x0,x1)) |
mark(0) |
mark(true) |
mark(s(x0)) |
mark(false) |
mark(inf(x0)) |
mark(cons(x0,x1)) |
mark(take(x0,x1)) |
mark(nil) |
mark(length(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
length#(active(X)) | → | length#(X) | (87) |
1 | > | 1 | |
length#(mark(X)) | → | length#(X) | (86) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.