The rewrite relation of the following TRS is considered.
active(nats) | → | mark(adx(zeros)) | (1) |
active(zeros) | → | mark(cons(0,zeros)) | (2) |
active(incr(cons(X,Y))) | → | mark(cons(s(X),incr(Y))) | (3) |
active(adx(cons(X,Y))) | → | mark(incr(cons(X,adx(Y)))) | (4) |
active(hd(cons(X,Y))) | → | mark(X) | (5) |
active(tl(cons(X,Y))) | → | mark(Y) | (6) |
mark(nats) | → | active(nats) | (7) |
mark(adx(X)) | → | active(adx(mark(X))) | (8) |
mark(zeros) | → | active(zeros) | (9) |
mark(cons(X1,X2)) | → | active(cons(X1,X2)) | (10) |
mark(0) | → | active(0) | (11) |
mark(incr(X)) | → | active(incr(mark(X))) | (12) |
mark(s(X)) | → | active(s(X)) | (13) |
mark(hd(X)) | → | active(hd(mark(X))) | (14) |
mark(tl(X)) | → | active(tl(mark(X))) | (15) |
adx(mark(X)) | → | adx(X) | (16) |
adx(active(X)) | → | adx(X) | (17) |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
incr(mark(X)) | → | incr(X) | (22) |
incr(active(X)) | → | incr(X) | (23) |
s(mark(X)) | → | s(X) | (24) |
s(active(X)) | → | s(X) | (25) |
hd(mark(X)) | → | hd(X) | (26) |
hd(active(X)) | → | hd(X) | (27) |
tl(mark(X)) | → | tl(X) | (28) |
tl(active(X)) | → | tl(X) | (29) |
active#(zeros) | → | cons#(0,zeros) | (30) |
active#(adx(cons(X,Y))) | → | cons#(X,adx(Y)) | (31) |
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
mark#(adx(X)) | → | active#(adx(mark(X))) | (33) |
active#(adx(cons(X,Y))) | → | incr#(cons(X,adx(Y))) | (34) |
active#(adx(cons(X,Y))) | → | mark#(incr(cons(X,adx(Y)))) | (35) |
mark#(adx(X)) | → | mark#(X) | (36) |
mark#(tl(X)) | → | active#(tl(mark(X))) | (37) |
mark#(zeros) | → | active#(zeros) | (38) |
mark#(tl(X)) | → | mark#(X) | (39) |
mark#(hd(X)) | → | active#(hd(mark(X))) | (40) |
incr#(active(X)) | → | incr#(X) | (41) |
mark#(incr(X)) | → | incr#(mark(X)) | (42) |
adx#(active(X)) | → | adx#(X) | (43) |
hd#(active(X)) | → | hd#(X) | (44) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (45) |
mark#(incr(X)) | → | mark#(X) | (46) |
active#(incr(cons(X,Y))) | → | s#(X) | (47) |
mark#(hd(X)) | → | hd#(mark(X)) | (48) |
active#(incr(cons(X,Y))) | → | cons#(s(X),incr(Y)) | (49) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (50) |
active#(hd(cons(X,Y))) | → | mark#(X) | (51) |
mark#(0) | → | active#(0) | (52) |
mark#(tl(X)) | → | tl#(mark(X)) | (53) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
active#(nats) | → | mark#(adx(zeros)) | (55) |
mark#(s(X)) | → | active#(s(X)) | (56) |
active#(adx(cons(X,Y))) | → | adx#(Y) | (57) |
adx#(mark(X)) | → | adx#(X) | (58) |
incr#(mark(X)) | → | incr#(X) | (59) |
active#(nats) | → | adx#(zeros) | (60) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (61) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (62) |
active#(incr(cons(X,Y))) | → | incr#(Y) | (63) |
mark#(cons(X1,X2)) | → | active#(cons(X1,X2)) | (64) |
hd#(mark(X)) | → | hd#(X) | (65) |
mark#(adx(X)) | → | adx#(mark(X)) | (66) |
tl#(mark(X)) | → | tl#(X) | (67) |
s#(active(X)) | → | s#(X) | (68) |
tl#(active(X)) | → | tl#(X) | (69) |
active#(zeros) | → | mark#(cons(0,zeros)) | (70) |
s#(mark(X)) | → | s#(X) | (71) |
mark#(hd(X)) | → | mark#(X) | (72) |
active#(tl(cons(X,Y))) | → | mark#(Y) | (73) |
mark#(nats) | → | active#(nats) | (74) |
The dependency pairs are split into 7 components.
mark#(nats) | → | active#(nats) | (74) |
active#(tl(cons(X,Y))) | → | mark#(Y) | (73) |
mark#(hd(X)) | → | mark#(X) | (72) |
mark#(incr(X)) | → | mark#(X) | (46) |
active#(zeros) | → | mark#(cons(0,zeros)) | (70) |
mark#(hd(X)) | → | active#(hd(mark(X))) | (40) |
mark#(cons(X1,X2)) | → | active#(cons(X1,X2)) | (64) |
mark#(tl(X)) | → | mark#(X) | (39) |
mark#(zeros) | → | active#(zeros) | (38) |
mark#(tl(X)) | → | active#(tl(mark(X))) | (37) |
mark#(s(X)) | → | active#(s(X)) | (56) |
mark#(adx(X)) | → | mark#(X) | (36) |
active#(nats) | → | mark#(adx(zeros)) | (55) |
active#(adx(cons(X,Y))) | → | mark#(incr(cons(X,adx(Y)))) | (35) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
mark#(adx(X)) | → | active#(adx(mark(X))) | (33) |
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
active#(hd(cons(X,Y))) | → | mark#(X) | (51) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | 33955 |
[hd(x1)] | = | 33955 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 33954 |
[adx(x1)] | = | 33955 |
[zeros] | = | 33955 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | 33955 |
[0] | = | 33957 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | 33955 |
[mark(x1)] | = | 33956 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 33955 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | 33954 |
[active#(x1)] | = | x1 + 0 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
hd(mark(X)) | → | hd(X) | (26) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
hd(active(X)) | → | hd(X) | (27) |
incr(mark(X)) | → | incr(X) | (22) |
tl(mark(X)) | → | tl(X) | (28) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
s(active(X)) | → | s(X) | (25) |
incr(active(X)) | → | incr(X) | (23) |
s(mark(X)) | → | s(X) | (24) |
tl(active(X)) | → | tl(X) | (29) |
mark#(cons(X1,X2)) | → | active#(cons(X1,X2)) | (64) |
mark#(s(X)) | → | active#(s(X)) | (56) |
The dependency pairs are split into 1 component.
active#(adx(cons(X,Y))) | → | mark#(incr(cons(X,adx(Y)))) | (35) |
mark#(tl(X)) | → | mark#(X) | (39) |
mark#(tl(X)) | → | active#(tl(mark(X))) | (37) |
mark#(adx(X)) | → | mark#(X) | (36) |
mark#(adx(X)) | → | active#(adx(mark(X))) | (33) |
active#(nats) | → | mark#(adx(zeros)) | (55) |
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
active#(hd(cons(X,Y))) | → | mark#(X) | (51) |
mark#(nats) | → | active#(nats) | (74) |
mark#(hd(X)) | → | mark#(X) | (72) |
mark#(hd(X)) | → | active#(hd(mark(X))) | (40) |
mark#(incr(X)) | → | mark#(X) | (46) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
active#(tl(cons(X,Y))) | → | mark#(Y) | (73) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 0 |
[hd(x1)] | = | x1 + 31598 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 0 |
[adx(x1)] | = | x1 + 29534 |
[zeros] | = | 24766 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 0 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 28224 |
[mark(x1)] | = | x1 + 0 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 54301 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | x1 + x2 + 0 |
[active#(x1)] | = | x1 + 0 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
active(adx(cons(X,Y))) | → | mark(incr(cons(X,adx(Y)))) | (4) |
mark(tl(X)) | → | active(tl(mark(X))) | (15) |
mark(adx(X)) | → | active(adx(mark(X))) | (8) |
active(nats) | → | mark(adx(zeros)) | (1) |
active(incr(cons(X,Y))) | → | mark(cons(s(X),incr(Y))) | (3) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
hd(mark(X)) | → | hd(X) | (26) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
hd(active(X)) | → | hd(X) | (27) |
incr(mark(X)) | → | incr(X) | (22) |
tl(mark(X)) | → | tl(X) | (28) |
active(hd(cons(X,Y))) | → | mark(X) | (5) |
mark(cons(X1,X2)) | → | active(cons(X1,X2)) | (10) |
mark(nats) | → | active(nats) | (7) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
s(active(X)) | → | s(X) | (25) |
mark(hd(X)) | → | active(hd(mark(X))) | (14) |
mark(incr(X)) | → | active(incr(mark(X))) | (12) |
incr(active(X)) | → | incr(X) | (23) |
s(mark(X)) | → | s(X) | (24) |
mark(0) | → | active(0) | (11) |
mark(zeros) | → | active(zeros) | (9) |
mark(s(X)) | → | active(s(X)) | (13) |
active(tl(cons(X,Y))) | → | mark(Y) | (6) |
tl(active(X)) | → | tl(X) | (29) |
active(zeros) | → | mark(cons(0,zeros)) | (2) |
mark#(tl(X)) | → | mark#(X) | (39) |
mark#(adx(X)) | → | mark#(X) | (36) |
active#(nats) | → | mark#(adx(zeros)) | (55) |
active#(hd(cons(X,Y))) | → | mark#(X) | (51) |
mark#(hd(X)) | → | mark#(X) | (72) |
active#(tl(cons(X,Y))) | → | mark#(Y) | (73) |
The dependency pairs are split into 1 component.
active#(adx(cons(X,Y))) | → | mark#(incr(cons(X,adx(Y)))) | (35) |
mark#(tl(X)) | → | active#(tl(mark(X))) | (37) |
mark#(adx(X)) | → | active#(adx(mark(X))) | (33) |
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
mark#(hd(X)) | → | active#(hd(mark(X))) | (40) |
mark#(incr(X)) | → | mark#(X) | (46) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 0 |
[hd(x1)] | = | x1 + 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 0 |
[adx(x1)] | = | 19507 |
[zeros] | = | 15837 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 24389 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | 11650 |
[mark(x1)] | = | x1 + 0 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 19506 |
[active(x1)] | = | x1 + 0 |
[cons(x1, x2)] | = | 0 |
[active#(x1)] | = | 0 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
mark#(tl(X)) | → | active#(tl(mark(X))) | (37) |
mark#(adx(X)) | → | active#(adx(mark(X))) | (33) |
mark#(hd(X)) | → | active#(hd(mark(X))) | (40) |
The dependency pairs are split into 1 component.
active#(adx(cons(X,Y))) | → | mark#(incr(cons(X,adx(Y)))) | (35) |
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
mark#(incr(X)) | → | mark#(X) | (46) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | 29358 |
[hd(x1)] | = | 29021 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 27857 |
[adx(x1)] | = | 29359 |
[zeros] | = | 0 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | 29358 |
[0] | = | 5599 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | 41476 |
[mark(x1)] | = | x1 + 1 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 13214 |
[active(x1)] | = | x1 + 1 |
[cons(x1, x2)] | = | x2 + 0 |
[active#(x1)] | = | x1 + 0 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
hd(mark(X)) | → | hd(X) | (26) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
hd(active(X)) | → | hd(X) | (27) |
incr(mark(X)) | → | incr(X) | (22) |
tl(mark(X)) | → | tl(X) | (28) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
s(active(X)) | → | s(X) | (25) |
incr(active(X)) | → | incr(X) | (23) |
s(mark(X)) | → | s(X) | (24) |
tl(active(X)) | → | tl(X) | (29) |
active#(adx(cons(X,Y))) | → | mark#(incr(cons(X,adx(Y)))) | (35) |
The dependency pairs are split into 1 component.
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
mark#(incr(X)) | → | mark#(X) | (46) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 42903 |
[hd(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 2805 |
[adx(x1)] | = | 11577 |
[zeros] | = | 42899 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 3024 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 26356 |
[mark(x1)] | = | x1 + 46517 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 11575 |
[active(x1)] | = | x1 + 46518 |
[cons(x1, x2)] | = | 42901 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
active#(incr(cons(X,Y))) | → | mark#(cons(s(X),incr(Y))) | (32) |
mark#(incr(X)) | → | mark#(X) | (46) |
mark#(incr(X)) | → | active#(incr(mark(X))) | (54) |
The dependency pairs are split into 0 components.
hd#(active(X)) | → | hd#(X) | (44) |
hd#(mark(X)) | → | hd#(X) | (65) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 2 |
[hd(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 2805 |
[adx(x1)] | = | 3 |
[zeros] | = | 1 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 44080 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 36404 |
[mark(x1)] | = | x1 + 46517 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | x1 + 0 |
[nats] | = | 1 |
[active(x1)] | = | x1 + 46518 |
[cons(x1, x2)] | = | 3 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
hd#(active(X)) | → | hd#(X) | (44) |
hd#(mark(X)) | → | hd#(X) | (65) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (71) |
s#(active(X)) | → | s#(X) | (68) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 38809 |
[hd(x1)] | = | 5969 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 2805 |
[adx(x1)] | = | 42387 |
[zeros] | = | 3578 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 17644 |
[s#(x1)] | = | x1 + 0 |
[tl(x1)] | = | x1 + 38368 |
[mark(x1)] | = | x1 + 46517 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 42385 |
[active(x1)] | = | x1 + 46518 |
[cons(x1, x2)] | = | 3580 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
s#(mark(X)) | → | s#(X) | (71) |
s#(active(X)) | → | s#(X) | (68) |
The dependency pairs are split into 0 components.
incr#(active(X)) | → | incr#(X) | (41) |
incr#(mark(X)) | → | incr#(X) | (59) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 977 |
[hd(x1)] | = | 41777 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 2805 |
[adx(x1)] | = | 38484 |
[zeros] | = | 32528 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 17644 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 29596 |
[mark(x1)] | = | x1 + 46517 |
[incr#(x1)] | = | x1 + 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 38482 |
[active(x1)] | = | x1 + 46518 |
[cons(x1, x2)] | = | 37509 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
incr#(active(X)) | → | incr#(X) | (41) |
incr#(mark(X)) | → | incr#(X) | (59) |
The dependency pairs are split into 0 components.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (50) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (45) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (62) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (61) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 28236 |
[hd(x1)] | = | 14264 |
[cons#(x1, x2)] | = | x2 + 0 |
[s(x1)] | = | 18292 |
[adx(x1)] | = | 29299 |
[zeros] | = | 1063 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 37662 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 57534 |
[mark(x1)] | = | x1 + 46517 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 1 |
[active(x1)] | = | x1 + 46518 |
[cons(x1, x2)] | = | 1065 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (50) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (61) |
The dependency pairs are split into 1 component.
cons#(mark(X1),X2) | → | cons#(X1,X2) | (45) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (62) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 10733 |
[hd(x1)] | = | 41701 |
[cons#(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | 48563 |
[adx(x1)] | = | 10734 |
[zeros] | = | 1 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 60627 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 23842 |
[mark(x1)] | = | x1 + 23975 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 10732 |
[active(x1)] | = | x1 + 23976 |
[cons(x1, x2)] | = | 3 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (45) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (62) |
The dependency pairs are split into 0 components.
adx#(active(X)) | → | adx#(X) | (43) |
adx#(mark(X)) | → | adx#(X) | (58) |
[adx#(x1)] | = | x1 + 0 |
[incr(x1)] | = | x1 + 10733 |
[hd(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[adx(x1)] | = | 8857 |
[zeros] | = | 22882 |
[tl#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 40096 |
[mark(x1)] | = | x1 + 1 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 8855 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 22884 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
adx#(active(X)) | → | adx#(X) | (43) |
adx#(mark(X)) | → | adx#(X) | (58) |
The dependency pairs are split into 0 components.
tl#(active(X)) | → | tl#(X) | (69) |
tl#(mark(X)) | → | tl#(X) | (67) |
[adx#(x1)] | = | 0 |
[incr(x1)] | = | x1 + 47313 |
[hd(x1)] | = | 35937 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1800 |
[adx(x1)] | = | 47315 |
[zeros] | = | 2 |
[tl#(x1)] | = | x1 + 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 36060 |
[s#(x1)] | = | 0 |
[tl(x1)] | = | x1 + 18436 |
[mark(x1)] | = | x1 + 1 |
[incr#(x1)] | = | 0 |
[hd#(x1)] | = | 0 |
[nats] | = | 47313 |
[active(x1)] | = | x1 + 2 |
[cons(x1, x2)] | = | 4 |
[active#(x1)] | = | 42902 |
cons(mark(X1),X2) | → | cons(X1,X2) | (18) |
adx(mark(X)) | → | adx(X) | (16) |
cons(X1,active(X2)) | → | cons(X1,X2) | (21) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (19) |
adx(active(X)) | → | adx(X) | (17) |
incr(mark(X)) | → | incr(X) | (22) |
cons(active(X1),X2) | → | cons(X1,X2) | (20) |
incr(active(X)) | → | incr(X) | (23) |
tl#(active(X)) | → | tl#(X) | (69) |
tl#(mark(X)) | → | tl#(X) | (67) |
The dependency pairs are split into 0 components.