The rewrite relation of the following TRS is considered.
active(nats) | → | mark(cons(0,incr(nats))) | (1) |
active(pairs) | → | mark(cons(0,incr(odds))) | (2) |
active(odds) | → | mark(incr(pairs)) | (3) |
active(incr(cons(X,XS))) | → | mark(cons(s(X),incr(XS))) | (4) |
active(head(cons(X,XS))) | → | mark(X) | (5) |
active(tail(cons(X,XS))) | → | mark(XS) | (6) |
mark(nats) | → | active(nats) | (7) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (8) |
mark(0) | → | active(0) | (9) |
mark(incr(X)) | → | active(incr(mark(X))) | (10) |
mark(pairs) | → | active(pairs) | (11) |
mark(odds) | → | active(odds) | (12) |
mark(s(X)) | → | active(s(mark(X))) | (13) |
mark(head(X)) | → | active(head(mark(X))) | (14) |
mark(tail(X)) | → | active(tail(mark(X))) | (15) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
incr(mark(X)) | → | incr(X) | (20) |
incr(active(X)) | → | incr(X) | (21) |
s(mark(X)) | → | s(X) | (22) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
head(active(X)) | → | head(X) | (25) |
tail(mark(X)) | → | tail(X) | (26) |
tail(active(X)) | → | tail(X) | (27) |
active#(pairs) | → | cons#(0,incr(odds)) | (28) |
active#(incr(cons(X,XS))) | → | s#(X) | (29) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (30) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (31) |
active#(incr(cons(X,XS))) | → | cons#(s(X),incr(XS)) | (32) |
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
mark#(cons(X1,X2)) | → | mark#(X1) | (34) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (35) |
mark#(s(X)) | → | s#(mark(X)) | (36) |
mark#(tail(X)) | → | mark#(X) | (37) |
mark#(head(X)) | → | active#(head(mark(X))) | (38) |
mark#(pairs) | → | active#(pairs) | (39) |
s#(active(X)) | → | s#(X) | (40) |
tail#(active(X)) | → | tail#(X) | (41) |
s#(mark(X)) | → | s#(X) | (42) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (43) |
mark#(odds) | → | active#(odds) | (44) |
active#(odds) | → | incr#(pairs) | (45) |
mark#(head(X)) | → | head#(mark(X)) | (46) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (48) |
mark#(incr(X)) | → | incr#(mark(X)) | (49) |
mark#(s(X)) | → | mark#(X) | (50) |
mark#(tail(X)) | → | tail#(mark(X)) | (51) |
head#(mark(X)) | → | head#(X) | (52) |
active#(nats) | → | cons#(0,incr(nats)) | (53) |
mark#(s(X)) | → | active#(s(mark(X))) | (54) |
active#(incr(cons(X,XS))) | → | incr#(XS) | (55) |
incr#(active(X)) | → | incr#(X) | (56) |
active#(head(cons(X,XS))) | → | mark#(X) | (57) |
active#(nats) | → | incr#(nats) | (58) |
tail#(mark(X)) | → | tail#(X) | (59) |
incr#(mark(X)) | → | incr#(X) | (60) |
active#(nats) | → | mark#(cons(0,incr(nats))) | (61) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (63) |
mark#(cons(X1,X2)) | → | cons#(mark(X1),X2) | (64) |
mark#(incr(X)) | → | mark#(X) | (65) |
head#(active(X)) | → | head#(X) | (66) |
active#(pairs) | → | incr#(odds) | (67) |
active#(pairs) | → | mark#(cons(0,incr(odds))) | (68) |
mark#(0) | → | active#(0) | (69) |
mark#(head(X)) | → | mark#(X) | (70) |
active#(tail(cons(X,XS))) | → | mark#(XS) | (71) |
mark#(nats) | → | active#(nats) | (72) |
The dependency pairs are split into 6 components.
mark#(nats) | → | active#(nats) | (72) |
active#(tail(cons(X,XS))) | → | mark#(XS) | (71) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(head(X)) | → | mark#(X) | (70) |
mark#(odds) | → | active#(odds) | (44) |
active#(pairs) | → | mark#(cons(0,incr(odds))) | (68) |
mark#(incr(X)) | → | mark#(X) | (65) |
mark#(pairs) | → | active#(pairs) | (39) |
mark#(head(X)) | → | active#(head(mark(X))) | (38) |
active#(nats) | → | mark#(cons(0,incr(nats))) | (61) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
mark#(tail(X)) | → | mark#(X) | (37) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (35) |
active#(head(cons(X,XS))) | → | mark#(X) | (57) |
mark#(s(X)) | → | active#(s(mark(X))) | (54) |
mark#(cons(X1,X2)) | → | mark#(X1) | (34) |
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
mark#(s(X)) | → | mark#(X) | (50) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (31) |
[incr(x1)] | = | 2 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[pairs] | = | 2 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 2 |
[mark#(x1)] | = | 2 |
[0] | = | 4 |
[s#(x1)] | = | 0 |
[odds] | = | 2 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | 3 |
[incr#(x1)] | = | 0 |
[nats] | = | 2 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | 2 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
mark#(s(X)) | → | active#(s(mark(X))) | (54) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (31) |
The dependency pairs are split into 1 component.
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
mark#(tail(X)) | → | mark#(X) | (37) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (35) |
mark#(cons(X1,X2)) | → | mark#(X1) | (34) |
active#(nats) | → | mark#(cons(0,incr(nats))) | (61) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
active#(head(cons(X,XS))) | → | mark#(X) | (57) |
mark#(incr(X)) | → | mark#(X) | (65) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
mark#(nats) | → | active#(nats) | (72) |
mark#(head(X)) | → | mark#(X) | (70) |
mark#(head(X)) | → | active#(head(mark(X))) | (38) |
mark#(odds) | → | active#(odds) | (44) |
mark#(pairs) | → | active#(pairs) | (39) |
mark#(s(X)) | → | mark#(X) | (50) |
active#(tail(cons(X,XS))) | → | mark#(XS) | (71) |
active#(pairs) | → | mark#(cons(0,incr(odds))) | (68) |
[incr(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[pairs] | = | 24479 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | x1 + 21238 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 0 |
[s#(x1)] | = | 0 |
[odds] | = | 24479 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[incr#(x1)] | = | 0 |
[nats] | = | 42151 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | x1 + 12457 |
[cons(x1, x2)] | = | x1 + x2 + 0 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
active(incr(cons(X,XS))) | → | mark(cons(s(X),incr(XS))) | (4) |
mark(tail(X)) | → | active(tail(mark(X))) | (15) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (8) |
active(nats) | → | mark(cons(0,incr(nats))) | (1) |
active(odds) | → | mark(incr(pairs)) | (3) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
active(head(cons(X,XS))) | → | mark(X) | (5) |
mark(incr(X)) | → | active(incr(mark(X))) | (10) |
mark(nats) | → | active(nats) | (7) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
mark(head(X)) | → | active(head(mark(X))) | (14) |
mark(odds) | → | active(odds) | (12) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
mark(pairs) | → | active(pairs) | (11) |
mark(0) | → | active(0) | (9) |
mark(s(X)) | → | active(s(mark(X))) | (13) |
active(tail(cons(X,XS))) | → | mark(XS) | (6) |
active(pairs) | → | mark(cons(0,incr(odds))) | (2) |
mark#(tail(X)) | → | mark#(X) | (37) |
active#(head(cons(X,XS))) | → | mark#(X) | (57) |
mark#(head(X)) | → | mark#(X) | (70) |
active#(tail(cons(X,XS))) | → | mark#(XS) | (71) |
The dependency pairs are split into 1 component.
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (35) |
mark#(cons(X1,X2)) | → | mark#(X1) | (34) |
active#(nats) | → | mark#(cons(0,incr(nats))) | (61) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(incr(X)) | → | mark#(X) | (65) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
mark#(nats) | → | active#(nats) | (72) |
mark#(head(X)) | → | active#(head(mark(X))) | (38) |
mark#(odds) | → | active#(odds) | (44) |
mark#(pairs) | → | active#(pairs) | (39) |
mark#(s(X)) | → | mark#(X) | (50) |
active#(pairs) | → | mark#(cons(0,incr(odds))) | (68) |
[incr(x1)] | = | 32798 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[pairs] | = | 32798 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 1 |
[mark#(x1)] | = | 32798 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[odds] | = | 32798 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | 1 |
[incr#(x1)] | = | 0 |
[nats] | = | 32798 |
[active(x1)] | = | 1 |
[head(x1)] | = | 12213 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
active(incr(cons(X,XS))) | → | mark(cons(s(X),incr(XS))) | (4) |
mark(tail(X)) | → | active(tail(mark(X))) | (15) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (8) |
active(nats) | → | mark(cons(0,incr(nats))) | (1) |
active(odds) | → | mark(incr(pairs)) | (3) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
active(head(cons(X,XS))) | → | mark(X) | (5) |
mark(incr(X)) | → | active(incr(mark(X))) | (10) |
mark(nats) | → | active(nats) | (7) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
mark(head(X)) | → | active(head(mark(X))) | (14) |
mark(odds) | → | active(odds) | (12) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
mark(pairs) | → | active(pairs) | (11) |
mark(0) | → | active(0) | (9) |
mark(s(X)) | → | active(s(mark(X))) | (13) |
active(tail(cons(X,XS))) | → | mark(XS) | (6) |
active(pairs) | → | mark(cons(0,incr(odds))) | (2) |
mark#(tail(X)) | → | active#(tail(mark(X))) | (35) |
mark#(head(X)) | → | active#(head(mark(X))) | (38) |
The dependency pairs are split into 1 component.
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
mark#(cons(X1,X2)) | → | mark#(X1) | (34) |
active#(nats) | → | mark#(cons(0,incr(nats))) | (61) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(incr(X)) | → | mark#(X) | (65) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
mark#(nats) | → | active#(nats) | (72) |
mark#(odds) | → | active#(odds) | (44) |
mark#(pairs) | → | active#(pairs) | (39) |
mark#(s(X)) | → | mark#(X) | (50) |
active#(pairs) | → | mark#(cons(0,incr(odds))) | (68) |
[incr(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[pairs] | = | 14221 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | x1 + 10451 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 14219 |
[s#(x1)] | = | 0 |
[odds] | = | 14221 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[incr#(x1)] | = | 0 |
[nats] | = | 14221 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | x1 + 62898 |
[cons(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
active(incr(cons(X,XS))) | → | mark(cons(s(X),incr(XS))) | (4) |
mark(tail(X)) | → | active(tail(mark(X))) | (15) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (8) |
active(nats) | → | mark(cons(0,incr(nats))) | (1) |
active(odds) | → | mark(incr(pairs)) | (3) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
active(head(cons(X,XS))) | → | mark(X) | (5) |
mark(incr(X)) | → | active(incr(mark(X))) | (10) |
mark(nats) | → | active(nats) | (7) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
mark(head(X)) | → | active(head(mark(X))) | (14) |
mark(odds) | → | active(odds) | (12) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
mark(pairs) | → | active(pairs) | (11) |
mark(0) | → | active(0) | (9) |
mark(s(X)) | → | active(s(mark(X))) | (13) |
active(tail(cons(X,XS))) | → | mark(XS) | (6) |
active(pairs) | → | mark(cons(0,incr(odds))) | (2) |
mark#(cons(X1,X2)) | → | mark#(X1) | (34) |
The dependency pairs are split into 1 component.
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(incr(X)) | → | mark#(X) | (65) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
mark#(odds) | → | active#(odds) | (44) |
mark#(s(X)) | → | mark#(X) | (50) |
[incr(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[pairs] | = | 0 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 2748 |
[s#(x1)] | = | 0 |
[odds] | = | 45380 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 45381 |
[incr#(x1)] | = | 0 |
[nats] | = | 1496 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | 0 |
[cons(x1, x2)] | = | 0 |
[active#(x1)] | = | 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
incr(mark(X)) | → | incr(X) | (20) |
mark#(odds) | → | active#(odds) | (44) |
mark#(s(X)) | → | mark#(X) | (50) |
The dependency pairs are split into 1 component.
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(incr(X)) | → | mark#(X) | (65) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
[incr(x1)] | = | x1 + 31744 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[pairs] | = | 0 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 14843 |
[s#(x1)] | = | 0 |
[odds] | = | 10336 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 31983 |
[incr#(x1)] | = | 0 |
[nats] | = | 20534 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | 0 |
[cons(x1, x2)] | = | x1 + 31742 |
[active#(x1)] | = | 31744 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
incr(mark(X)) | → | incr(X) | (20) |
s(active(X)) | → | s(X) | (23) |
active#(incr(cons(X,XS))) | → | mark#(cons(s(X),incr(XS))) | (33) |
mark#(incr(X)) | → | mark#(X) | (65) |
The dependency pairs are split into 1 component.
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
[incr(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[pairs] | = | 1 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 23637 |
[mark#(x1)] | = | 2 |
[0] | = | 14843 |
[s#(x1)] | = | 0 |
[odds] | = | 10336 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[incr#(x1)] | = | 0 |
[nats] | = | 20534 |
[active(x1)] | = | 0 |
[head(x1)] | = | 0 |
[cons(x1, x2)] | = | 15620 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
active#(odds) | → | mark#(incr(pairs)) | (47) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (62) |
The dependency pairs are split into 0 components.
head#(active(X)) | → | head#(X) | (66) |
head#(mark(X)) | → | head#(X) | (52) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 21102 |
[pairs] | = | 16335 |
[head#(x1)] | = | x1 + 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 9534 |
[s#(x1)] | = | 0 |
[odds] | = | 25192 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25194 |
[incr#(x1)] | = | 0 |
[nats] | = | 19621 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | 0 |
[cons(x1, x2)] | = | 44798 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
head#(active(X)) | → | head#(X) | (66) |
head#(mark(X)) | → | head#(X) | (52) |
The dependency pairs are split into 0 components.
tail#(active(X)) | → | tail#(X) | (41) |
tail#(mark(X)) | → | tail#(X) | (59) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 26815 |
[pairs] | = | 1338 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 9534 |
[s#(x1)] | = | 0 |
[odds] | = | 3969 |
[tail#(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 25194 |
[incr#(x1)] | = | 0 |
[nats] | = | 11668 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | 0 |
[cons(x1, x2)] | = | 436 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
tail#(active(X)) | → | tail#(X) | (41) |
tail#(mark(X)) | → | tail#(X) | (59) |
The dependency pairs are split into 0 components.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (48) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (43) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (63) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (30) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | 1 |
[pairs] | = | 1338 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[odds] | = | 1 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25194 |
[incr#(x1)] | = | 0 |
[nats] | = | 7335 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 0 |
cons(active(X1),X2) | → | cons(X1,X2) | (18) |
cons(mark(X1),X2) | → | cons(X1,X2) | (16) |
incr(active(X)) | → | incr(X) | (21) |
tail(mark(X)) | → | tail(X) | (26) |
cons(X1,active(X2)) | → | cons(X1,X2) | (19) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (17) |
tail(active(X)) | → | tail(X) | (27) |
s(mark(X)) | → | s(X) | (22) |
incr(mark(X)) | → | incr(X) | (20) |
head(active(X)) | → | head(X) | (25) |
s(active(X)) | → | s(X) | (23) |
head(mark(X)) | → | head(X) | (24) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (43) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (30) |
The dependency pairs are split into 1 component.
cons#(X1,active(X2)) | → | cons#(X1,X2) | (63) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (48) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | x2 + 0 |
[s(x1)] | = | 1 |
[pairs] | = | 2 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 35971 |
[s#(x1)] | = | 0 |
[odds] | = | 13825 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 13826 |
[incr#(x1)] | = | 0 |
[nats] | = | 14264 |
[active(x1)] | = | x1 + 0 |
[head(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + 1647 |
[active#(x1)] | = | 0 |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (48) |
The dependency pairs are split into 1 component.
cons#(X1,active(X2)) | → | cons#(X1,X2) | (63) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | x2 + 0 |
[s(x1)] | = | 1 |
[pairs] | = | 2 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 24376 |
[s#(x1)] | = | 0 |
[odds] | = | 13825 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 13827 |
[incr#(x1)] | = | 0 |
[nats] | = | 48949 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + 10748 |
[active#(x1)] | = | 0 |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (63) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (42) |
s#(active(X)) | → | s#(X) | (40) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 28255 |
[pairs] | = | 11495 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 1 |
[s#(x1)] | = | x1 + 0 |
[odds] | = | 1002 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 13827 |
[incr#(x1)] | = | 0 |
[nats] | = | 8573 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
s#(mark(X)) | → | s#(X) | (42) |
s#(active(X)) | → | s#(X) | (40) |
The dependency pairs are split into 0 components.
incr#(mark(X)) | → | incr#(X) | (60) |
incr#(active(X)) | → | incr#(X) | (56) |
[incr(x1)] | = | 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 39707 |
[pairs] | = | 1 |
[head#(x1)] | = | 0 |
[tail(x1)] | = | 0 |
[mark#(x1)] | = | 2 |
[0] | = | 44797 |
[s#(x1)] | = | 0 |
[odds] | = | 1911 |
[tail#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 13827 |
[incr#(x1)] | = | x1 + 0 |
[nats] | = | 8573 |
[active(x1)] | = | x1 + 1 |
[head(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
incr#(mark(X)) | → | incr#(X) | (60) |
incr#(active(X)) | → | incr#(X) | (56) |
The dependency pairs are split into 0 components.