The rewrite relation of the following TRS is considered.
a__from(X) | → | cons(mark(X),from(s(X))) | (1) |
a__length(nil) | → | 0 | (2) |
a__length(cons(X,Y)) | → | s(a__length1(Y)) | (3) |
a__length1(X) | → | a__length(X) | (4) |
mark(from(X)) | → | a__from(mark(X)) | (5) |
mark(length(X)) | → | a__length(X) | (6) |
mark(length1(X)) | → | a__length1(X) | (7) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (8) |
mark(s(X)) | → | s(mark(X)) | (9) |
mark(nil) | → | nil | (10) |
mark(0) | → | 0 | (11) |
a__from(X) | → | from(X) | (12) |
a__length(X) | → | length(X) | (13) |
a__length1(X) | → | length1(X) | (14) |
mark#(s(X)) | → | mark#(X) | (15) |
a__length#(cons(X,Y)) | → | a__length1#(Y) | (16) |
a__length1#(X) | → | a__length#(X) | (17) |
a__from#(X) | → | mark#(X) | (18) |
mark#(from(X)) | → | mark#(X) | (19) |
mark#(length1(X)) | → | a__length1#(X) | (20) |
mark#(length(X)) | → | a__length#(X) | (21) |
mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
mark#(from(X)) | → | a__from#(mark(X)) | (23) |
The dependency pairs are split into 2 components.
mark#(from(X)) | → | a__from#(mark(X)) | (23) |
mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
mark#(from(X)) | → | mark#(X) | (19) |
a__from#(X) | → | mark#(X) | (18) |
mark#(s(X)) | → | mark#(X) | (15) |
[a__length1#(x1)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[a__from#(x1)] | = | x1 + 1 |
[a__from(x1)] | = | x1 + 3 |
[length1(x1)] | = | 1 |
[a__length1(x1)] | = | 1 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[from(x1)] | = | x1 + 3 |
[nil] | = | 44083 |
[mark(x1)] | = | x1 + 1 |
[a__length#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 2 |
[length(x1)] | = | 1 |
[a__length(x1)] | = | 1 |
a__length1(X) | → | a__length(X) | (4) |
mark(cons(X1,X2)) | → | cons(mark(X1),X2) | (8) |
a__from(X) | → | cons(mark(X),from(s(X))) | (1) |
a__length(cons(X,Y)) | → | s(a__length1(Y)) | (3) |
mark(from(X)) | → | a__from(mark(X)) | (5) |
mark(nil) | → | nil | (10) |
mark(length1(X)) | → | a__length1(X) | (7) |
a__length1(X) | → | length1(X) | (14) |
a__from(X) | → | from(X) | (12) |
mark(0) | → | 0 | (11) |
mark(s(X)) | → | s(mark(X)) | (9) |
a__length(X) | → | length(X) | (13) |
mark(length(X)) | → | a__length(X) | (6) |
a__length(nil) | → | 0 | (2) |
mark#(from(X)) | → | a__from#(mark(X)) | (23) |
mark#(cons(X1,X2)) | → | mark#(X1) | (22) |
mark#(from(X)) | → | mark#(X) | (19) |
a__from#(X) | → | mark#(X) | (18) |
The dependency pairs are split into 1 component.
mark#(s(X)) | → | mark#(X) | (15) |
[a__length1#(x1)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[a__from#(x1)] | = | 1 |
[a__from(x1)] | = | 44603 |
[length1(x1)] | = | 1 |
[a__length1(x1)] | = | 1 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 3 |
[from(x1)] | = | 14681 |
[nil] | = | 44083 |
[mark(x1)] | = | x1 + 29922 |
[a__length#(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 26288 |
[length(x1)] | = | 3000 |
[a__length(x1)] | = | 2 |
mark#(s(X)) | → | mark#(X) | (15) |
The dependency pairs are split into 0 components.
a__length1#(X) | → | a__length#(X) | (17) |
a__length#(cons(X,Y)) | → | a__length1#(Y) | (16) |
[a__length1#(x1)] | = | x1 + 1 |
[s(x1)] | = | x1 + 9727 |
[a__from#(x1)] | = | 1 |
[a__from(x1)] | = | 33603 |
[length1(x1)] | = | 1 |
[a__length1(x1)] | = | 1 |
[mark#(x1)] | = | 0 |
[0] | = | 9728 |
[from(x1)] | = | 33602 |
[nil] | = | 28882 |
[mark(x1)] | = | x1 + 1 |
[a__length#(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + x2 + 2242 |
[length(x1)] | = | 9728 |
[a__length(x1)] | = | 9727 |
a__length1#(X) | → | a__length#(X) | (17) |
a__length#(cons(X,Y)) | → | a__length1#(Y) | (16) |
The dependency pairs are split into 0 components.