The rewrite relation of the following TRS is considered.
There are 133 ruless (increase limit for explicit display).
There are 207 ruless (increase limit for explicit display).
The dependency pairs are split into 23 components.
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (336) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (332) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(take(X1,X2)) | → | mark#(X1) | (225) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
mark#(U81(X)) | → | mark#(X) | (320) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (318) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
mark#(U72(X1,X2)) | → | mark#(X1) | (311) |
mark#(zeros) | → | active#(zeros) | (205) |
mark#(s(X)) | → | active#(s(mark(X))) | (309) |
mark#(take(X1,X2)) | → | mark#(X2) | (200) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (305) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
mark#(U21(X)) | → | mark#(X) | (197) |
mark#(U81(X)) | → | active#(U81(mark(X))) | (196) |
mark#(U21(X)) | → | active#(U21(mark(X))) | (195) |
active#(zeros) | → | mark#(cons(0,zeros)) | (297) |
mark#(U62(X)) | → | mark#(X) | (191) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (292) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (185) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (180) |
mark#(U62(X)) | → | active#(U62(mark(X))) | (282) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (278) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U11(X)) | → | mark#(X) | (171) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
mark#(U91(X1,X2,X3,X4)) | → | mark#(X1) | (167) |
mark#(U92(X1,X2,X3,X4)) | → | mark#(X1) | (273) |
mark#(U42(X)) | → | mark#(X) | (163) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
mark#(U52(X)) | → | mark#(X) | (270) |
active#(take(0,IL)) | → | mark#(U81(isNatIList(IL))) | (268) |
mark#(U93(X1,X2,X3,X4)) | → | mark#(X1) | (157) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
mark#(cons(X1,X2)) | → | mark#(X1) | (153) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (147) |
mark#(length(X)) | → | mark#(X) | (144) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U11(X)) | → | active#(U11(mark(X))) | (253) |
mark#(U31(X)) | → | active#(U31(mark(X))) | (141) |
mark#(U42(X)) | → | active#(U42(mark(X))) | (142) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (248) |
mark#(U31(X)) | → | mark#(X) | (245) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
mark#(U52(X)) | → | active#(U52(mark(X))) | (244) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 5911 |
[isNatList(x1)] | = | 48894 |
[U11(x1)] | = | 26531 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 15047 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 14459 |
[U91(x1,...,x4)] | = | 48894 |
[take(x1, x2)] | = | 48894 |
[U71(x1, x2, x3)] | = | 48894 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 48894 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | 48894 |
[U72(x1, x2)] | = | 48894 |
[zeros] | = | 48894 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 48894 |
[0] | = | 1 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[U62(x1)] | = | 32582 |
[mark(x1)] | = | 1 |
[isNat(x1)] | = | 48894 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | 48894 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | 0 |
[U31(x1)] | = | 48893 |
[U92(x1,...,x4)] | = | 48894 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 32135 |
[active#(x1)] | = | x1 + 0 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 1 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | 48894 |
[length(x1)] | = | 48894 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 48894 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U81(mark(X)) | → | U81(X) | (104) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
s(mark(X)) | → | s(X) | (100) |
U81(active(X)) | → | U81(X) | (105) |
U21(active(X)) | → | U21(X) | (63) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U11(mark(X)) | → | U11(X) | (60) |
U62(active(X)) | → | U62(X) | (87) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U31(active(X)) | → | U31(X) | (65) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U31(mark(X)) | → | U31(X) | (64) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U91(X1,X2,mark(X3),X4) | → | U91(X1,X2,X3,X4) | (108) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
U21(mark(X)) | → | U21(X) | (62) |
U91(mark(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (106) |
U91(X1,active(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (111) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U42(mark(X)) | → | U42(X) | (70) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U91(X1,X2,X3,mark(X4)) | → | U91(X1,X2,X3,X4) | (109) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
isNat(mark(X)) | → | isNat(X) | (98) |
U91(X1,mark(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (107) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
U91(active(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (110) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U11(active(X)) | → | U11(X) | (61) |
U91(X1,X2,X3,active(X4)) | → | U91(X1,X2,X3,X4) | (113) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U91(X1,X2,active(X3),X4) | → | U91(X1,X2,X3,X4) | (112) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U62(mark(X)) | → | U62(X) | (86) |
mark#(s(X)) | → | active#(s(mark(X))) | (309) |
mark#(U81(X)) | → | active#(U81(mark(X))) | (196) |
mark#(U21(X)) | → | active#(U21(mark(X))) | (195) |
mark#(U62(X)) | → | active#(U62(mark(X))) | (282) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (147) |
mark#(U11(X)) | → | active#(U11(mark(X))) | (253) |
mark#(U31(X)) | → | active#(U31(mark(X))) | (141) |
mark#(U42(X)) | → | active#(U42(mark(X))) | (142) |
mark#(U52(X)) | → | active#(U52(mark(X))) | (244) |
The dependency pairs are split into 1 component.
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
mark#(U81(X)) | → | mark#(X) | (320) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (278) |
mark#(U93(X1,X2,X3,X4)) | → | mark#(X1) | (157) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (332) |
active#(zeros) | → | mark#(cons(0,zeros)) | (297) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (305) |
mark#(U31(X)) | → | mark#(X) | (245) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
active#(take(0,IL)) | → | mark#(U81(isNatIList(IL))) | (268) |
mark#(U62(X)) | → | mark#(X) | (191) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(U11(X)) | → | mark#(X) | (171) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
mark#(length(X)) | → | mark#(X) | (144) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
mark#(U91(X1,X2,X3,X4)) | → | mark#(X1) | (167) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (185) |
mark#(zeros) | → | active#(zeros) | (205) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (336) |
mark#(cons(X1,X2)) | → | mark#(X1) | (153) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (248) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(take(X1,X2)) | → | mark#(X2) | (200) |
mark#(take(X1,X2)) | → | mark#(X1) | (225) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (318) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U92(X1,X2,X3,X4)) | → | mark#(X1) | (273) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (292) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | mark#(X1) | (311) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (180) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[isNatList(x1)] | = | 47701 |
[U11(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[U91(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 17892 |
[take(x1, x2)] | = | x1 + x2 + 65593 |
[U71(x1, x2, x3)] | = | x1 + x2 + x3 + 19222 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 47701 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 17892 |
[U72(x1, x2)] | = | x1 + x2 + 19222 |
[zeros] | = | 39229 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 48894 |
[0] | = | 0 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 10392 |
[U62(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 47701 |
[U52(x1)] | = | x1 + 0 |
[U61(x1, x2)] | = | x1 + 0 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1)] | = | x1 + 0 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 17892 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 0 |
[active#(x1)] | = | x1 + 48894 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 12148 |
[tt] | = | 47701 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + 0 |
[length(x1)] | = | x1 + 66923 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x1 + 0 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
There are 133 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(U81(X)) | → | mark#(X) | (320) |
mark#(U93(X1,X2,X3,X4)) | → | mark#(X1) | (157) |
active#(take(0,IL)) | → | mark#(U81(isNatIList(IL))) | (268) |
mark#(length(X)) | → | mark#(X) | (144) |
mark#(U91(X1,X2,X3,X4)) | → | mark#(X1) | (167) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (248) |
mark#(take(X1,X2)) | → | mark#(X2) | (200) |
mark#(take(X1,X2)) | → | mark#(X1) | (225) |
mark#(U92(X1,X2,X3,X4)) | → | mark#(X1) | (273) |
mark#(U72(X1,X2)) | → | mark#(X1) | (311) |
The dependency pairs are split into 1 component.
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (278) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (332) |
active#(zeros) | → | mark#(cons(0,zeros)) | (297) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (305) |
mark#(U31(X)) | → | mark#(X) | (245) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
mark#(U62(X)) | → | mark#(X) | (191) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(U11(X)) | → | mark#(X) | (171) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (185) |
mark#(zeros) | → | active#(zeros) | (205) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (336) |
mark#(cons(X1,X2)) | → | mark#(X1) | (153) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (318) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (292) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (180) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[isNatList(x1)] | = | 4685 |
[U11(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[U91(x1,...,x4)] | = | x4 + 1 |
[take(x1, x2)] | = | x2 + 0 |
[U71(x1, x2, x3)] | = | 25292 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 4685 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x4 + 1 |
[U72(x1, x2)] | = | 25292 |
[zeros] | = | 4455 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 48894 |
[0] | = | 4453 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 0 |
[U62(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 4685 |
[U52(x1)] | = | x1 + 0 |
[U61(x1, x2)] | = | x1 + 0 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1)] | = | x1 + 0 |
[U92(x1,...,x4)] | = | x4 + 1 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x1 + 1 |
[active#(x1)] | = | x1 + 48894 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 0 |
[tt] | = | 4685 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + 0 |
[length(x1)] | = | 25292 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x1 + 0 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
There are 133 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsactive#(zeros) | → | mark#(cons(0,zeros)) | (297) |
mark#(cons(X1,X2)) | → | mark#(X1) | (153) |
The dependency pairs are split into 1 component.
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
active#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (278) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (332) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (305) |
mark#(U31(X)) | → | mark#(X) | (245) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
mark#(U62(X)) | → | mark#(X) | (191) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(U11(X)) | → | mark#(X) | (171) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (185) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (336) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (318) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (292) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (180) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[isNatList(x1)] | = | 50844 |
[U11(x1)] | = | x1 + 0 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[U91(x1,...,x4)] | = | x4 + 1939 |
[take(x1, x2)] | = | x2 + 14046 |
[U71(x1, x2, x3)] | = | 592 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 50844 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x4 + 1937 |
[U72(x1, x2)] | = | 592 |
[zeros] | = | 4455 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 48894 |
[0] | = | 1 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 0 |
[U62(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 50844 |
[U52(x1)] | = | x1 + 0 |
[U61(x1, x2)] | = | x1 + 0 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1)] | = | x1 + 0 |
[U92(x1,...,x4)] | = | x4 + 1938 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x1 + 1936 |
[active#(x1)] | = | x1 + 48894 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 0 |
[tt] | = | 50844 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + 0 |
[length(x1)] | = | 592 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x1 + 0 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
There are 133 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsactive#(U92(tt,IL,M,N)) | → | mark#(U93(isNat(N),IL,M,N)) | (278) |
active#(U93(tt,IL,M,N)) | → | mark#(cons(N,take(M,IL))) | (305) |
active#(U91(tt,IL,M,N)) | → | mark#(U92(isNat(M),IL,M,N)) | (336) |
active#(take(s(M),cons(N,IL))) | → | mark#(U91(isNatIList(IL),IL,M,N)) | (180) |
The dependency pairs are split into 1 component.
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (332) |
mark#(U31(X)) | → | mark#(X) | (245) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
mark#(U62(X)) | → | mark#(X) | (191) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(U11(X)) | → | mark#(X) | (171) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (185) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (318) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (292) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 9396 |
[isNatList(x1)] | = | 9399 |
[U11(x1)] | = | 9398 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 24386 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 9396 |
[U91(x1,...,x4)] | = | 9396 |
[take(x1, x2)] | = | 2839 |
[U71(x1, x2, x3)] | = | 9399 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 9399 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | 9398 |
[U72(x1, x2)] | = | 9399 |
[zeros] | = | 1395 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 48894 |
[0] | = | 9398 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 9396 |
[U62(x1)] | = | 9396 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 9399 |
[U52(x1)] | = | 9396 |
[U61(x1, x2)] | = | 9399 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | 9398 |
[U31(x1)] | = | 9396 |
[U92(x1,...,x4)] | = | 8426 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 9398 |
[active#(x1)] | = | x1 + 39495 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 9396 |
[tt] | = | 9398 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | 9399 |
[length(x1)] | = | 9399 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 9399 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U81(mark(X)) | → | U81(X) | (104) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
s(mark(X)) | → | s(X) | (100) |
U81(active(X)) | → | U81(X) | (105) |
U21(active(X)) | → | U21(X) | (63) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U11(mark(X)) | → | U11(X) | (60) |
U62(active(X)) | → | U62(X) | (87) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U31(active(X)) | → | U31(X) | (65) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U31(mark(X)) | → | U31(X) | (64) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U91(X1,X2,mark(X3),X4) | → | U91(X1,X2,X3,X4) | (108) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
U21(mark(X)) | → | U21(X) | (62) |
U91(mark(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (106) |
U91(X1,active(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (111) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U42(mark(X)) | → | U42(X) | (70) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U91(X1,X2,X3,mark(X4)) | → | U91(X1,X2,X3,X4) | (109) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
isNat(mark(X)) | → | isNat(X) | (98) |
U91(X1,mark(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (107) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
U91(active(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (110) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U11(active(X)) | → | U11(X) | (61) |
U91(X1,X2,X3,active(X4)) | → | U91(X1,X2,X3,X4) | (113) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U91(X1,X2,active(X3),X4) | → | U91(X1,X2,X3,X4) | (112) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U62(mark(X)) | → | U62(X) | (86) |
mark#(U93(X1,X2,X3,X4)) | → | active#(U93(mark(X1),X2,X3,X4)) | (332) |
mark#(U91(X1,X2,X3,X4)) | → | active#(U91(mark(X1),X2,X3,X4)) | (185) |
mark#(take(X1,X2)) | → | active#(take(mark(X1),mark(X2))) | (318) |
mark#(U92(X1,X2,X3,X4)) | → | active#(U92(mark(X1),X2,X3,X4)) | (292) |
The dependency pairs are split into 1 component.
active#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
mark#(U31(X)) | → | mark#(X) | (245) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
mark#(U62(X)) | → | mark#(X) | (191) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(U11(X)) | → | mark#(X) | (171) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[isNatList(x1)] | = | x1 + 2 |
[U11(x1)] | = | x1 + 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[U91(x1,...,x4)] | = | x2 + x3 + x4 + 30393 |
[take(x1, x2)] | = | x1 + x2 + 30393 |
[U71(x1, x2, x3)] | = | x2 + x3 + 3 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | x1 + 4 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x3 + x4 + 30393 |
[U72(x1, x2)] | = | x2 + 3 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 39495 |
[0] | = | 0 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[U62(x1)] | = | x1 + 1 |
[mark(x1)] | = | x1 + 0 |
[isNat(x1)] | = | x1 + 1 |
[U52(x1)] | = | x1 + 0 |
[U61(x1, x2)] | = | x1 + x2 + 5 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1)] | = | x1 + 1 |
[U92(x1,...,x4)] | = | x2 + x3 + x4 + 30393 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 0 |
[active#(x1)] | = | x1 + 39495 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 1 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 1 |
[length(x1)] | = | x1 + 3 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x1 + x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
There are 133 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsactive#(isNat(length(V1))) | → | mark#(U11(isNatList(V1))) | (323) |
mark#(U31(X)) | → | mark#(X) | (245) |
mark#(U62(X)) | → | mark#(X) | (191) |
mark#(U11(X)) | → | mark#(X) | (171) |
active#(isNatIList(V)) | → | mark#(U31(isNatList(V))) | (306) |
active#(isNatList(take(V1,V2))) | → | mark#(U61(isNat(V1),V2)) | (178) |
active#(U61(tt,V2)) | → | mark#(U62(isNatIList(V2))) | (140) |
mark#(U51(X1,X2)) | → | mark#(X1) | (174) |
mark#(U41(X1,X2)) | → | mark#(X1) | (239) |
mark#(U61(X1,X2)) | → | mark#(X1) | (265) |
The dependency pairs are split into 1 component.
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 3101 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[U91(x1,...,x4)] | = | x2 + x4 + 52455 |
[take(x1, x2)] | = | 35727 |
[U71(x1, x2, x3)] | = | 1 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + 52459 |
[U72(x1, x2)] | = | 1 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 39495 |
[0] | = | 11433 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 35731 |
[U62(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | x1 + 0 |
[U61(x1, x2)] | = | x1 + 2 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 8666 |
[U92(x1,...,x4)] | = | x2 + x3 + x4 + 52457 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 52461 |
[active#(x1)] | = | 39496 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 35729 |
[tt] | = | 8668 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | 1 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 1 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U81(mark(X)) | → | U81(X) | (104) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
s(mark(X)) | → | s(X) | (100) |
U81(active(X)) | → | U81(X) | (105) |
U21(active(X)) | → | U21(X) | (63) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U11(mark(X)) | → | U11(X) | (60) |
U62(active(X)) | → | U62(X) | (87) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U31(active(X)) | → | U31(X) | (65) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U31(mark(X)) | → | U31(X) | (64) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U91(X1,X2,mark(X3),X4) | → | U91(X1,X2,X3,X4) | (108) |
U21(mark(X)) | → | U21(X) | (62) |
U91(mark(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (106) |
U91(X1,active(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (111) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U42(mark(X)) | → | U42(X) | (70) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U91(X1,X2,X3,mark(X4)) | → | U91(X1,X2,X3,X4) | (109) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
isNat(mark(X)) | → | isNat(X) | (98) |
U91(X1,mark(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (107) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U91(active(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (110) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U11(active(X)) | → | U11(X) | (61) |
U91(X1,X2,X3,active(X4)) | → | U91(X1,X2,X3,X4) | (113) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U91(X1,X2,active(X3),X4) | → | U91(X1,X2,X3,X4) | (112) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U62(mark(X)) | → | U62(X) | (86) |
mark#(U61(X1,X2)) | → | active#(U61(mark(X1),X2)) | (312) |
The dependency pairs are split into 1 component.
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
[U72#(x1, x2)] | = | max(0) |
[U21(x1)] | = | x1 + 0 |
[isNatList(x1)] | = | x1 + 0 |
[U11(x1)] | = | 442 |
[cons#(x1, x2)] | = | max(0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | max(0) |
[U42(x1)] | = | x1 + 2 |
[U91(x1,...,x4)] | = | max(x1 + 2, x3 + 1, x4 + 5, 0) |
[take(x1, x2)] | = | max(0) |
[U71(x1, x2, x3)] | = | max(0) |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | max(0) |
[isNatIList(x1)] | = | x1 + 2 |
[U93#(x1,...,x4)] | = | max(0) |
[U93(x1,...,x4)] | = | max(x2 + 0, x3 + 1288, 0) |
[U72(x1, x2)] | = | max(0) |
[zeros] | = | 4 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 4 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 632 |
[U62(x1)] | = | 3 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 259 |
[U52(x1)] | = | x1 + 1 |
[U61(x1, x2)] | = | max(x2 + 4, 0) |
[U51#(x1, x2)] | = | max(0) |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 4 |
[U31(x1)] | = | 6 |
[U92(x1,...,x4)] | = | max(x1 + 648, x2 + 642, x3 + 645, x4 + 646, 0) |
[U41#(x1, x2)] | = | max(0) |
[cons(x1, x2)] | = | max(x1 + 7, x2 + 4, 0) |
[active#(x1)] | = | x1 + 0 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 628 |
[tt] | = | 636 |
[U71#(x1, x2, x3)] | = | max(0) |
[U51(x1, x2)] | = | max(x2 + 2, 0) |
[length(x1)] | = | 0 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | max(x2 + 5, 0) |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | max(0) |
[U61#(x1, x2)] | = | max(0) |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U81(mark(X)) | → | U81(X) | (104) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
s(mark(X)) | → | s(X) | (100) |
U81(active(X)) | → | U81(X) | (105) |
U21(active(X)) | → | U21(X) | (63) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U21(mark(X)) | → | U21(X) | (62) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U42(mark(X)) | → | U42(X) | (70) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
isNat(mark(X)) | → | isNat(X) | (98) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
active#(isNatIList(cons(V1,V2))) | → | mark#(U41(isNat(V1),V2)) | (176) |
active#(U41(tt,V2)) | → | mark#(U42(isNatIList(V2))) | (326) |
active#(U51(tt,V2)) | → | mark#(U52(isNatList(V2))) | (271) |
active#(isNatList(cons(V1,V2))) | → | mark#(U51(isNat(V1),V2)) | (314) |
mark#(U42(X)) | → | mark#(X) | (163) |
mark#(U52(X)) | → | mark#(X) | (270) |
The dependency pairs are split into 1 component.
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 1 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 1 |
[U91(x1,...,x4)] | = | 1 |
[take(x1, x2)] | = | 1 |
[U71(x1, x2, x3)] | = | 11474 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 11473 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | 1 |
[U72(x1, x2)] | = | 11474 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 50969 |
[0] | = | 1 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 1 |
[U62(x1)] | = | 1 |
[mark(x1)] | = | 1 |
[isNat(x1)] | = | 11474 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | 1 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | 2 |
[U31(x1)] | = | 1 |
[U92(x1,...,x4)] | = | 1 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 39495 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 1 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | 9205 |
[length(x1)] | = | 11474 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 9086 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U81(mark(X)) | → | U81(X) | (104) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
s(mark(X)) | → | s(X) | (100) |
U81(active(X)) | → | U81(X) | (105) |
U21(active(X)) | → | U21(X) | (63) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U11(mark(X)) | → | U11(X) | (60) |
U62(active(X)) | → | U62(X) | (87) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U31(active(X)) | → | U31(X) | (65) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U31(mark(X)) | → | U31(X) | (64) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U91(X1,X2,mark(X3),X4) | → | U91(X1,X2,X3,X4) | (108) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
U21(mark(X)) | → | U21(X) | (62) |
U91(mark(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (106) |
U91(X1,active(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (111) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U42(mark(X)) | → | U42(X) | (70) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U91(X1,X2,X3,mark(X4)) | → | U91(X1,X2,X3,X4) | (109) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
isNat(mark(X)) | → | isNat(X) | (98) |
U91(X1,mark(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (107) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
U91(active(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (110) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U11(active(X)) | → | U11(X) | (61) |
U91(X1,X2,X3,active(X4)) | → | U91(X1,X2,X3,X4) | (113) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U91(X1,X2,active(X3),X4) | → | U91(X1,X2,X3,X4) | (112) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U62(mark(X)) | → | U62(X) | (86) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (240) |
mark#(U51(X1,X2)) | → | active#(U51(mark(X1),X2)) | (183) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (210) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (291) |
The dependency pairs are split into 1 component.
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
mark#(U21(X)) | → | mark#(X) | (197) |
[U72#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U21(x1)] | = |
|
||||||||||||||||||||||||||
[isNatList(x1)] | = |
|
||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||
[cons#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||
[isNat#(x1)] | = |
|
||||||||||||||||||||||||||
[take#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U42(x1)] | = |
|
||||||||||||||||||||||||||
[U91(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[take(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U71(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U81#(x1)] | = |
|
||||||||||||||||||||||||||
[U92#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||||||||||||||||
[U93#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U93(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U72(x1, x2)] | = |
|
||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||
[U52#(x1)] | = |
|
||||||||||||||||||||||||||
[U42#(x1)] | = |
|
||||||||||||||||||||||||||
[U62#(x1)] | = |
|
||||||||||||||||||||||||||
[mark#(x1)] | = |
|
||||||||||||||||||||||||||
[0] | = |
|
||||||||||||||||||||||||||
[isNatList#(x1)] | = |
|
||||||||||||||||||||||||||
[s#(x1)] | = |
|
||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||
[U62(x1)] | = |
|
||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||
[isNat(x1)] | = |
|
||||||||||||||||||||||||||
[U52(x1)] | = |
|
||||||||||||||||||||||||||
[U61(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U51#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U11#(x1)] | = |
|
||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||
[U31(x1)] | = |
|
||||||||||||||||||||||||||
[U92(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U41#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||
[active#(x1)] | = |
|
||||||||||||||||||||||||||
[isNatIList#(x1)] | = |
|
||||||||||||||||||||||||||
[U21#(x1)] | = |
|
||||||||||||||||||||||||||
[U81(x1)] | = |
|
||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||
[U71#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U51(x1, x2)] | = |
|
||||||||||||||||||||||||||
[length(x1)] | = |
|
||||||||||||||||||||||||||
[length#(x1)] | = |
|
||||||||||||||||||||||||||
[U41(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U31#(x1)] | = |
|
||||||||||||||||||||||||||
[U91#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U61#(x1, x2)] | = |
|
isNatList(mark(X)) | → | isNatList(X) | (80) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
s(mark(X)) | → | s(X) | (100) |
U21(active(X)) | → | U21(X) | (63) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U31(active(X)) | → | U31(X) | (65) |
U31(mark(X)) | → | U31(X) | (64) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U21(mark(X)) | → | U21(X) | (62) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
isNat(mark(X)) | → | isNat(X) | (98) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (182) |
mark#(U21(X)) | → | mark#(X) | (197) |
The dependency pairs are split into 1 component.
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 4 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 1 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 1 |
[U91(x1,...,x4)] | = | 1 |
[take(x1, x2)] | = | 1 |
[U71(x1, x2, x3)] | = | 17640 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 4 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | 1 |
[U72(x1, x2)] | = | 17640 |
[zeros] | = | 2 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 0 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 4 |
[U62(x1)] | = | 1 |
[mark(x1)] | = | 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | 1 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | 0 |
[U31(x1)] | = | 1 |
[U92(x1,...,x4)] | = | 1 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 1 |
[active#(x1)] | = | x1 + 50969 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 4 |
[tt] | = | 4 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | 1 |
[length(x1)] | = | 17640 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 1 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U81(mark(X)) | → | U81(X) | (104) |
length(active(X)) | → | length(X) | (103) |
length(mark(X)) | → | length(X) | (102) |
U92(X1,X2,X3,active(X4)) | → | U92(X1,X2,X3,X4) | (121) |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U51(X1,active(X2)) | → | U51(X1,X2) | (77) |
take(X1,mark(X2)) | → | take(X1,X2) | (131) |
U41(active(X1),X2) | → | U41(X1,X2) | (68) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U61(X1,active(X2)) | → | U61(X1,X2) | (85) |
s(mark(X)) | → | s(X) | (100) |
U81(active(X)) | → | U81(X) | (105) |
U21(active(X)) | → | U21(X) | (63) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U92(X1,X2,X3,mark(X4)) | → | U92(X1,X2,X3,X4) | (117) |
U11(mark(X)) | → | U11(X) | (60) |
U62(active(X)) | → | U62(X) | (87) |
U61(active(X1),X2) | → | U61(X1,X2) | (84) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U31(active(X)) | → | U31(X) | (65) |
U92(X1,X2,active(X3),X4) | → | U92(X1,X2,X3,X4) | (120) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
U31(mark(X)) | → | U31(X) | (64) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (93) |
U92(X1,active(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (119) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (92) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (88) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U91(X1,X2,mark(X3),X4) | → | U91(X1,X2,X3,X4) | (108) |
take(mark(X1),X2) | → | take(X1,X2) | (130) |
U21(mark(X)) | → | U21(X) | (62) |
U91(mark(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (106) |
U91(X1,active(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (111) |
U61(mark(X1),X2) | → | U61(X1,X2) | (82) |
take(X1,active(X2)) | → | take(X1,X2) | (133) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (89) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U52(active(X)) | → | U52(X) | (79) |
s(active(X)) | → | s(X) | (101) |
U41(X1,active(X2)) | → | U41(X1,X2) | (69) |
U72(active(X1),X2) | → | U72(X1,X2) | (96) |
U52(mark(X)) | → | U52(X) | (78) |
U92(active(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (118) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
U42(mark(X)) | → | U42(X) | (70) |
U72(mark(X1),X2) | → | U72(X1,X2) | (94) |
U91(X1,X2,X3,mark(X4)) | → | U91(X1,X2,X3,X4) | (109) |
U51(active(X1),X2) | → | U51(X1,X2) | (76) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
isNat(mark(X)) | → | isNat(X) | (98) |
U91(X1,mark(X2),X3,X4) | → | U91(X1,X2,X3,X4) | (107) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (90) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (67) |
take(active(X1),X2) | → | take(X1,X2) | (132) |
U91(active(X1),X2,X3,X4) | → | U91(X1,X2,X3,X4) | (110) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U92(X1,X2,mark(X3),X4) | → | U92(X1,X2,X3,X4) | (116) |
U11(active(X)) | → | U11(X) | (61) |
U91(X1,X2,X3,active(X4)) | → | U91(X1,X2,X3,X4) | (113) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U51(mark(X1),X2) | → | U51(X1,X2) | (74) |
U91(X1,X2,active(X3),X4) | → | U91(X1,X2,X3,X4) | (112) |
U51(X1,mark(X2)) | → | U51(X1,X2) | (75) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (91) |
U72(X1,active(X2)) | → | U72(X1,X2) | (97) |
isNat(active(X)) | → | isNat(X) | (99) |
U92(mark(X1),X2,X3,X4) | → | U92(X1,X2,X3,X4) | (114) |
U72(X1,mark(X2)) | → | U72(X1,X2) | (95) |
U92(X1,mark(X2),X3,X4) | → | U92(X1,X2,X3,X4) | (115) |
U41(mark(X1),X2) | → | U41(X1,X2) | (66) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (83) |
U62(mark(X)) | → | U62(X) | (86) |
mark#(isNat(X)) | → | active#(isNat(X)) | (222) |
The dependency pairs are split into 1 component.
active#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
[U72#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U21(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[isNatList(x1)] | = |
|
||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||
[cons#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[s(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[isNat#(x1)] | = |
|
||||||||||||||||||||||||||
[take#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U42(x1)] | = |
|
||||||||||||||||||||||||||
[U91(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[take(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U71(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U81#(x1)] | = |
|
||||||||||||||||||||||||||
[U92#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||||||||||||||||
[U93#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U93(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U72(x1, x2)] | = |
|
||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||
[U52#(x1)] | = |
|
||||||||||||||||||||||||||
[U42#(x1)] | = |
|
||||||||||||||||||||||||||
[U62#(x1)] | = |
|
||||||||||||||||||||||||||
[mark#(x1)] | = |
|
||||||||||||||||||||||||||
[0] | = |
|
||||||||||||||||||||||||||
[isNatList#(x1)] | = |
|
||||||||||||||||||||||||||
[s#(x1)] | = |
|
||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||
[U62(x1)] | = |
|
||||||||||||||||||||||||||
[mark(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[isNat(x1)] | = |
|
||||||||||||||||||||||||||
[U52(x1)] | = |
|
||||||||||||||||||||||||||
[U61(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U51#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U11#(x1)] | = |
|
||||||||||||||||||||||||||
[active(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[U31(x1)] | = |
|
||||||||||||||||||||||||||
[U92(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U41#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||
[active#(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[isNatIList#(x1)] | = |
|
||||||||||||||||||||||||||
[U21#(x1)] | = |
|
||||||||||||||||||||||||||
[U81(x1)] | = |
|
||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||
[U71#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U51(x1, x2)] | = |
|
||||||||||||||||||||||||||
[length(x1)] | = |
|
||||||||||||||||||||||||||
[length#(x1)] | = |
|
||||||||||||||||||||||||||
[U41(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U31#(x1)] | = |
|
||||||||||||||||||||||||||
[U91#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U61#(x1, x2)] | = |
|
There are 133 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsactive#(length(cons(N,L))) | → | mark#(U71(isNatList(L),L,N)) | (173) |
mark#(length(X)) | → | active#(length(mark(X))) | (172) |
active#(U72(tt,L)) | → | mark#(s(length(L))) | (255) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (135) |
active#(U71(tt,L,N)) | → | mark#(U72(isNat(N),L)) | (219) |
mark#(s(X)) | → | mark#(X) | (175) |
mark#(U72(X1,X2)) | → | active#(U72(mark(X1),X2)) | (230) |
The dependency pairs are split into 0 components.
U72#(active(X1),X2) | → | U72#(X1,X2) | (226) |
U72#(mark(X1),X2) | → | U72#(X1,X2) | (202) |
U72#(X1,mark(X2)) | → | U72#(X1,X2) | (293) |
U72#(X1,active(X2)) | → | U72#(X1,X2) | (269) |
[U72#(x1, x2)] | = | x1 + x2 + 0 |
[U21(x1)] | = | 56105 |
[isNatList(x1)] | = | 22402 |
[U11(x1)] | = | x1 + 8043 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 45374 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 1513 |
[U91(x1,...,x4)] | = | x2 + x4 + 92999 |
[take(x1, x2)] | = | x1 + 47623 |
[U71(x1, x2, x3)] | = | x3 + 45370 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1509 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x3 + x4 + 138381 |
[U72(x1, x2)] | = | 45372 |
[zeros] | = | 28810 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 19716 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 67343 |
[U62(x1)] | = | 22406 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 10729 |
[U52(x1)] | = | 22406 |
[U61(x1, x2)] | = | x2 + 22404 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 1511 |
[U92(x1,...,x4)] | = | x1 + x2 + 82272 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 138383 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 67341 |
[tt] | = | 56107 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 22404 |
[length(x1)] | = | 19714 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 1511 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U62(mark(X)) | → | U62(X) | (86) |
U72#(active(X1),X2) | → | U72#(X1,X2) | (226) |
U72#(mark(X1),X2) | → | U72#(X1,X2) | (202) |
U72#(X1,mark(X2)) | → | U72#(X1,X2) | (293) |
U72#(X1,active(X2)) | → | U72#(X1,X2) | (269) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (290) |
s#(active(X)) | → | s#(X) | (154) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 10 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | x1 + 26411 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 7 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x2 + x4 + 44755 |
[take(x1, x2)] | = | x1 + 31842 |
[U71(x1, x2, x3)] | = | x3 + 3 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x3 + x4 + 44770 |
[U72(x1, x2)] | = | 5 |
[zeros] | = | 15509 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 4 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | x1 + 0 |
[nil] | = | 31850 |
[U62(x1)] | = | 10 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 6 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 4 |
[U92(x1,...,x4)] | = | x1 + x2 + 44756 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 44772 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 31848 |
[tt] | = | 12 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U62(mark(X)) | → | U62(X) | (86) |
s#(mark(X)) | → | s#(X) | (290) |
s#(active(X)) | → | s#(X) | (154) |
The dependency pairs are split into 0 components.
U92#(X1,mark(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (339) |
U92#(X1,X2,mark(X3),X4) | → | U92#(X1,X2,X3,X4) | (238) |
U92#(X1,active(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (227) |
U92#(X1,X2,active(X3),X4) | → | U92#(X1,X2,X3,X4) | (316) |
U92#(mark(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (302) |
U92#(X1,X2,X3,active(X4)) | → | U92#(X1,X2,X3,X4) | (184) |
U92#(active(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (276) |
U92#(X1,X2,X3,mark(X4)) | → | U92#(X1,X2,X3,X4) | (262) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 10 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | x1 + 3 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 7 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 8 |
[U91(x1,...,x4)] | = | x2 + x4 + 10 |
[take(x1, x2)] | = | x1 + 1 |
[U71(x1, x2, x3)] | = | x3 + 3 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | x3 + x4 + 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x3 + x4 + 61685 |
[U72(x1, x2)] | = | 5 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 3 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 8 |
[U62(x1)] | = | 7 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 5 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 3 |
[U92(x1,...,x4)] | = | x1 + x2 + 29073 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 61687 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 6 |
[tt] | = | 12 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 6 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U62(mark(X)) | → | U62(X) | (86) |
U92#(X1,X2,mark(X3),X4) | → | U92#(X1,X2,X3,X4) | (238) |
U92#(X1,X2,active(X3),X4) | → | U92#(X1,X2,X3,X4) | (316) |
U92#(X1,X2,X3,active(X4)) | → | U92#(X1,X2,X3,X4) | (184) |
U92#(X1,X2,X3,mark(X4)) | → | U92#(X1,X2,X3,X4) | (262) |
The dependency pairs are split into 1 component.
U92#(X1,active(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (227) |
U92#(active(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (276) |
U92#(mark(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (302) |
U92#(X1,mark(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (339) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 3897 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | x1 + 1515 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | 2382 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 12 |
[U91(x1,...,x4)] | = | x2 + x4 + 2387 |
[take(x1, x2)] | = | x1 + 1 |
[U71(x1, x2, x3)] | = | x3 + 2378 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | x2 + 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x3 + x4 + 22459 |
[U72(x1, x2)] | = | 2380 |
[zeros] | = | 33217 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 3 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 8 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1513 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 12 |
[U92(x1,...,x4)] | = | x1 + x2 + 876 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 94903 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 6 |
[tt] | = | 3899 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 10 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U62(mark(X)) | → | U62(X) | (86) |
U92#(X1,active(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (227) |
U92#(X1,mark(X2),X3,X4) | → | U92#(X1,X2,X3,X4) | (339) |
The dependency pairs are split into 1 component.
U92#(active(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (276) |
U92#(mark(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (302) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 21111 |
[isNatList(x1)] | = | x1 + 1 |
[U11(x1)] | = | 36606 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 60993 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | x1 + 24380 |
[U91(x1,...,x4)] | = | x4 + 36603 |
[take(x1, x2)] | = | 36601 |
[U71(x1, x2, x3)] | = | x1 + x3 + 33148 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | x1 + 0 |
[isNatIList(x1)] | = | x1 + 26958 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 3 |
[U72(x1, x2)] | = | x1 + x2 + 33154 |
[zeros] | = | 7 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 45378 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 36605 |
[U62(x1)] | = | 36606 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 36604 |
[U52(x1)] | = | 24381 |
[U61(x1, x2)] | = | x2 + 36604 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 26960 |
[U92(x1,...,x4)] | = | x3 + 36605 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 24376 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 36603 |
[tt] | = | 36608 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | 24379 |
[length(x1)] | = | x1 + 8771 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 51336 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U11(mark(X)) | → | U11(X) | (60) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
U11(active(X)) | → | U11(X) | (61) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U92#(active(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (276) |
U92#(mark(X1),X2,X3,X4) | → | U92#(X1,X2,X3,X4) | (302) |
The dependency pairs are split into 0 components.
U61#(mark(X1),X2) | → | U61#(X1,X2) | (331) |
U61#(X1,mark(X2)) | → | U61#(X1,X2) | (221) |
U61#(active(X1),X2) | → | U61#(X1,X2) | (199) |
U61#(X1,active(X2)) | → | U61#(X1,X2) | (159) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 18683 |
[isNatList(x1)] | = | 34233 |
[U11(x1)] | = | 34236 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 18681 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 6767 |
[U91(x1,...,x4)] | = | x1 + 30985 |
[take(x1, x2)] | = | x1 + 19034 |
[U71(x1, x2, x3)] | = | x1 + x3 + 1 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 6732 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 99463 |
[U72(x1, x2)] | = | 34242 |
[zeros] | = | 47295 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 34234 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 80779 |
[U62(x1)] | = | 34237 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 2 |
[U52(x1)] | = | 34237 |
[U61(x1, x2)] | = | x2 + 34235 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 6734 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + 65224 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 114670 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 46538 |
[tt] | = | 34239 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 34235 |
[length(x1)] | = | 34232 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 6765 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | x1 + x2 + 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U11(active(X)) | → | U11(X) | (61) |
U61#(mark(X1),X2) | → | U61#(X1,X2) | (331) |
U61#(X1,mark(X2)) | → | U61#(X1,X2) | (221) |
U61#(active(X1),X2) | → | U61#(X1,X2) | (199) |
U61#(X1,active(X2)) | → | U61#(X1,X2) | (159) |
The dependency pairs are split into 0 components.
U51#(X1,active(X2)) | → | U51#(X1,X2) | (233) |
U51#(X1,mark(X2)) | → | U51#(X1,X2) | (189) |
U51#(active(X1),X2) | → | U51#(X1,X2) | (168) |
U51#(mark(X1),X2) | → | U51#(X1,X2) | (143) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 14 |
[isNatList(x1)] | = | 38627 |
[U11(x1)] | = | 38631 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 12 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 38631 |
[U91(x1,...,x4)] | = | x1 + 1 |
[take(x1, x2)] | = | x1 + 27743 |
[U71(x1, x2, x3)] | = | x1 + x3 + 3 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 38627 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 77269 |
[U72(x1, x2)] | = | 38638 |
[zeros] | = | 3036 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 38630 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 66383 |
[U62(x1)] | = | 38631 |
[mark(x1)] | = | x1 + 22184 |
[isNat(x1)] | = | x1 + 1 |
[U52(x1)] | = | 38631 |
[U61(x1, x2)] | = | x2 + 38629 |
[U51#(x1, x2)] | = | x1 + x2 + 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 22185 |
[U31(x1)] | = | 38629 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + 38635 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 88161 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 27748 |
[tt] | = | 38633 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 38629 |
[length(x1)] | = | 38628 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 38629 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U11(active(X)) | → | U11(X) | (61) |
U51#(X1,active(X2)) | → | U51#(X1,X2) | (233) |
U51#(X1,mark(X2)) | → | U51#(X1,X2) | (189) |
U51#(active(X1),X2) | → | U51#(X1,X2) | (168) |
U51#(mark(X1),X2) | → | U51#(X1,X2) | (143) |
The dependency pairs are split into 0 components.
U52#(mark(X)) | → | U52#(X) | (304) |
U52#(active(X)) | → | U52#(X) | (198) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 14 |
[isNatList(x1)] | = | 4 |
[U11(x1)] | = | 8 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 12 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 8 |
[U91(x1,...,x4)] | = | x1 + 38861 |
[take(x1, x2)] | = | x1 + 38851 |
[U71(x1, x2, x3)] | = | x1 + x3 + 1 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 4 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 38879 |
[U72(x1, x2)] | = | 13 |
[zeros] | = | 24887 |
[U52#(x1)] | = | x1 + 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 5 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 38866 |
[U62(x1)] | = | 8 |
[mark(x1)] | = | x1 + 21762 |
[isNat(x1)] | = | x1 + 3 |
[U52(x1)] | = | 8 |
[U61(x1, x2)] | = | x2 + 6 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 21763 |
[U31(x1)] | = | 6 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + 38870 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 40 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 38854 |
[tt] | = | 10 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 6 |
[length(x1)] | = | 3 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 6 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U11(active(X)) | → | U11(X) | (61) |
U52#(mark(X)) | → | U52#(X) | (304) |
U52#(active(X)) | → | U52#(X) | (198) |
The dependency pairs are split into 0 components.
U42#(mark(X)) | → | U42#(X) | (337) |
U42#(active(X)) | → | U42#(X) | (138) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 25172 |
[isNatList(x1)] | = | 64347 |
[U11(x1)] | = | 64351 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 25170 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 64351 |
[U91(x1,...,x4)] | = | x1 + 59775 |
[take(x1, x2)] | = | x1 + 37890 |
[U71(x1, x2, x3)] | = | x1 + x3 + 2 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 31784 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 188481 |
[U72(x1, x2)] | = | 89515 |
[zeros] | = | 45766 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | x1 + 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 64349 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 134812 |
[U62(x1)] | = | 64351 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 2 |
[U52(x1)] | = | 64351 |
[U61(x1, x2)] | = | x2 + 64349 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 31786 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + 124128 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 214946 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 70457 |
[tt] | = | 64353 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 64349 |
[length(x1)] | = | 64347 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 64349 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U11(active(X)) | → | U11(X) | (61) |
U42#(mark(X)) | → | U42#(X) | (337) |
U42#(active(X)) | → | U42#(X) | (138) |
The dependency pairs are split into 0 components.
U91#(active(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (237) |
U91#(X1,active(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (333) |
U91#(X1,mark(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (299) |
U91#(mark(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (192) |
U91#(X1,X2,X3,mark(X4)) | → | U91#(X1,X2,X3,X4) | (165) |
U91#(X1,X2,X3,active(X4)) | → | U91#(X1,X2,X3,X4) | (266) |
U91#(X1,X2,mark(X3),X4) | → | U91#(X1,X2,X3,X4) | (264) |
U91#(X1,X2,active(X3),X4) | → | U91#(X1,X2,X3,X4) | (148) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 14 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 5 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 12 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + 14 |
[take(x1, x2)] | = | x1 + 1 |
[U71(x1, x2, x3)] | = | x1 + x3 + 2 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 28 |
[U72(x1, x2)] | = | 11 |
[zeros] | = | 31691 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 3 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 3420 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 2 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 3 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + 21 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 36 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 5 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U11(active(X)) | → | U11(X) | (61) |
U91#(active(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (237) |
U91#(X1,active(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (333) |
U91#(X1,mark(X2),X3,X4) | → | U91#(X1,X2,X3,X4) | (299) |
U91#(mark(X1),X2,X3,X4) | → | U91#(X1,X2,X3,X4) | (192) |
U91#(X1,X2,X3,mark(X4)) | → | U91#(X1,X2,X3,X4) | (165) |
U91#(X1,X2,X3,active(X4)) | → | U91#(X1,X2,X3,X4) | (266) |
U91#(X1,X2,mark(X3),X4) | → | U91#(X1,X2,X3,X4) | (264) |
U91#(X1,X2,active(X3),X4) | → | U91#(X1,X2,X3,X4) | (148) |
The dependency pairs are split into 0 components.
isNatIList#(active(X)) | → | isNatIList#(X) | (235) |
isNatIList#(mark(X)) | → | isNatIList#(X) | (162) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | x1 + 31080 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 5 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 31078 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + 103327 |
[take(x1, x2)] | = | x1 + 53261 |
[U71(x1, x2, x3)] | = | x1 + x3 + 31068 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 103341 |
[U72(x1, x2)] | = | 31077 |
[zeros] | = | 25585 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 3 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 53274 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 30139 |
[isNat(x1)] | = | x1 + 2 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 30140 |
[U31(x1)] | = | 3 |
[U92(x1,...,x4)] | = | x1 + x2 + x3 + 103334 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 50089 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | x1 + 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 53265 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U11(active(X)) | → | U11(X) | (61) |
isNatIList#(active(X)) | → | isNatIList#(X) | (235) |
isNatIList#(mark(X)) | → | isNatIList#(X) | (162) |
The dependency pairs are split into 0 components.
length#(mark(X)) | → | length#(X) | (201) |
length#(active(X)) | → | length#(X) | (145) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 15701 |
[isNatList(x1)] | = | 1563 |
[U11(x1)] | = | x1 + 7510 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 39163 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 15701 |
[U91(x1,...,x4)] | = | x2 + x4 + 49309 |
[take(x1, x2)] | = | x2 + 81965 |
[U71(x1, x2, x3)] | = | x3 + 41666 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 2687 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 59757 |
[U72(x1, x2)] | = | x1 + 45607 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 41666 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 94979 |
[U62(x1)] | = | 13954 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 2566 |
[U52(x1)] | = | x1 + 32656 |
[U61(x1, x2)] | = | x1 + x2 + 5504 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 6507 |
[U31(x1)] | = | 9194 |
[U92(x1,...,x4)] | = | x3 + 55816 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 6507 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | 88472 |
[tt] | = | 22208 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 5504 |
[length(x1)] | = | 35159 |
[length#(x1)] | = | x1 + 0 |
[U41(x1, x2)] | = | x2 + 9194 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U93(X1,X2,mark(X3),X4) | → | U93(X1,X2,X3,X4) | (124) |
U93(mark(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (122) |
U93(X1,X2,X3,mark(X4)) | → | U93(X1,X2,X3,X4) | (125) |
U93(X1,active(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (127) |
U93(active(X1),X2,X3,X4) | → | U93(X1,X2,X3,X4) | (126) |
U93(X1,X2,X3,active(X4)) | → | U93(X1,X2,X3,X4) | (129) |
U93(X1,X2,active(X3),X4) | → | U93(X1,X2,X3,X4) | (128) |
isNat(mark(X)) | → | isNat(X) | (98) |
U93(X1,mark(X2),X3,X4) | → | U93(X1,X2,X3,X4) | (123) |
isNat(active(X)) | → | isNat(X) | (99) |
length#(mark(X)) | → | length#(X) | (201) |
length#(active(X)) | → | length#(X) | (145) |
The dependency pairs are split into 0 components.
U41#(mark(X1),X2) | → | U41#(X1,X2) | (194) |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (190) |
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (170) |
U41#(active(X1),X2) | → | U41#(X1,X2) | (256) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 3 |
[isNatList(x1)] | = | 2162 |
[U11(x1)] | = | 2167 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2188 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 2167 |
[U91(x1,...,x4)] | = | x1 + 3443 |
[take(x1, x2)] | = | 5604 |
[U71(x1, x2, x3)] | = | x3 + 50620 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 2163 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 5616 |
[U72(x1, x2)] | = | x1 + x2 + 50621 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 56220 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 5614 |
[U62(x1)] | = | 2167 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | 2167 |
[U61(x1, x2)] | = | x2 + 2165 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 2165 |
[U92(x1,...,x4)] | = | x2 + x3 + 5614 |
[U41#(x1, x2)] | = | x1 + x2 + 0 |
[cons(x1, x2)] | = | x2 + 14 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 3443 |
[tt] | = | 2169 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 2165 |
[length(x1)] | = | x1 + 50604 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 2165 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
U41#(mark(X1),X2) | → | U41#(X1,X2) | (194) |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (190) |
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (170) |
U41#(active(X1),X2) | → | U41#(X1,X2) | (256) |
The dependency pairs are split into 0 components.
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (234) |
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (208) |
U71#(X1,mark(X2),X3) | → | U71#(X1,X2,X3) | (303) |
U71#(X1,active(X2),X3) | → | U71#(X1,X2,X3) | (186) |
U71#(active(X1),X2,X3) | → | U71#(X1,X2,X3) | (137) |
U71#(mark(X1),X2,X3) | → | U71#(X1,X2,X3) | (246) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 3 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 3 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 31677 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + 23665 |
[take(x1, x2)] | = | 1 |
[U71(x1, x2, x3)] | = | x3 + 31668 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 31664 |
[U72(x1, x2)] | = | x1 + x2 + 31669 |
[zeros] | = | 22191 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 14 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 11 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 4 |
[U92(x1,...,x4)] | = | x2 + x3 + 31662 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 31665 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 2 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | x1 + x2 + 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | x1 + 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
U71#(X1,mark(X2),X3) | → | U71#(X1,X2,X3) | (303) |
U71#(X1,active(X2),X3) | → | U71#(X1,X2,X3) | (186) |
U71#(active(X1),X2,X3) | → | U71#(X1,X2,X3) | (137) |
U71#(mark(X1),X2,X3) | → | U71#(X1,X2,X3) | (246) |
The dependency pairs are split into 1 component.
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (208) |
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (234) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 50070 |
[isNatList(x1)] | = | 15280 |
[U11(x1)] | = | 50070 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 348342 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 58724 |
[U91(x1,...,x4)] | = | x1 + 39896 |
[take(x1, x2)] | = | 18637 |
[U71(x1, x2, x3)] | = | x3 + 244473 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 5402 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 188481 |
[U72(x1, x2)] | = | x1 + x2 + 247725 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 209788 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 161820 |
[U62(x1)] | = | 68602 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 23409 |
[U52(x1)] | = | 68602 |
[U61(x1, x2)] | = | x2 + 41941 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 26661 |
[U31(x1)] | = | 32063 |
[U92(x1,...,x4)] | = | x2 + x3 + 161820 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 196505 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 39896 |
[tt] | = | 95263 |
[U71#(x1, x2, x3)] | = | x3 + 0 |
[U51(x1, x2)] | = | x2 + 41941 |
[length(x1)] | = | x1 + 21307 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 32063 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (208) |
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (234) |
The dependency pairs are split into 0 components.
U21#(mark(X)) | → | U21#(X) | (242) |
U21#(active(X)) | → | U21#(X) | (272) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 4066 |
[isNatList(x1)] | = | 4569 |
[U11(x1)] | = | 3 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 29447 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 4573 |
[U91(x1,...,x4)] | = | x1 + 2980 |
[take(x1, x2)] | = | 7547 |
[U71(x1, x2, x3)] | = | x3 + 30110 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 4569 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 7559 |
[U72(x1, x2)] | = | x1 + x2 + 30111 |
[zeros] | = | 41433 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 21320 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 7557 |
[U62(x1)] | = | 4573 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | 4573 |
[U61(x1, x2)] | = | x2 + 4571 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 4571 |
[U92(x1,...,x4)] | = | x2 + x3 + 7557 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 24867 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | x1 + 0 |
[U81(x1)] | = | x1 + 2980 |
[tt] | = | 4575 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 4571 |
[length(x1)] | = | x1 + 5241 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 4571 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
U21#(mark(X)) | → | U21#(X) | (242) |
U21#(active(X)) | → | U21#(X) | (272) |
The dependency pairs are split into 0 components.
U62#(active(X)) | → | U62#(X) | (279) |
U62#(mark(X)) | → | U62#(X) | (134) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 4 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 5 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 13223 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + 2 |
[take(x1, x2)] | = | 1 |
[U71(x1, x2, x3)] | = | x3 + 16289 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 13 |
[U72(x1, x2)] | = | x1 + x2 + 16290 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | x1 + 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 36852 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 20577 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 3 |
[U92(x1,...,x4)] | = | x2 + x3 + 11 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 14 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 20568 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | x1 + 16273 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
U62#(active(X)) | → | U62#(X) | (279) |
U62#(mark(X)) | → | U62#(X) | (134) |
The dependency pairs are split into 0 components.
cons#(X1,active(X2)) | → | cons#(X1,X2) | (193) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (155) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (151) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (136) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 1954 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 1955 |
[cons#(x1, x2)] | = | x1 + x2 + 0 |
[s(x1)] | = | x1 + 38909 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 6 |
[U91(x1,...,x4)] | = | x1 + 32494 |
[take(x1, x2)] | = | 1 |
[U71(x1, x2, x3)] | = | x3 + 46743 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 2 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 36676 |
[U72(x1, x2)] | = | x1 + x2 + 44793 |
[zeros] | = | 38108 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 36852 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 4730 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1952 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 4 |
[U92(x1,...,x4)] | = | x2 + x3 + 36674 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 36677 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 550 |
[tt] | = | 4178 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | x1 + 10064 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 4 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (193) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (155) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (151) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (136) |
The dependency pairs are split into 0 components.
take#(X1,active(X2)) | → | take#(X1,X2) | (220) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (298) |
take#(active(X1),X2) | → | take#(X1,X2) | (158) |
take#(mark(X1),X2) | → | take#(X1,X2) | (257) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 3 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 3 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 8552 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | x2 + 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + 4862 |
[take(x1, x2)] | = | 1 |
[U71(x1, x2, x3)] | = | x3 + 33165 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x2 + x4 + 8470 |
[U72(x1, x2)] | = | x1 + x2 + 33166 |
[zeros] | = | 40775 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 36852 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 560 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 1 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 4 |
[U92(x1,...,x4)] | = | x2 + x3 + 8468 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 8471 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 2 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x2 + 3 |
[length(x1)] | = | x1 + 24692 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U62(active(X)) | → | U62(X) | (87) |
isNatIList(mark(X)) | → | isNatIList(X) | (72) |
cons(mark(X1),X2) | → | cons(X1,X2) | (56) |
U42(mark(X)) | → | U42(X) | (70) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (57) |
cons(X1,active(X2)) | → | cons(X1,X2) | (59) |
cons(active(X1),X2) | → | cons(X1,X2) | (58) |
U42(active(X)) | → | U42(X) | (71) |
isNatIList(active(X)) | → | isNatIList(X) | (73) |
U62(mark(X)) | → | U62(X) | (86) |
take#(X1,active(X2)) | → | take#(X1,X2) | (220) |
take#(X1,mark(X2)) | → | take#(X1,X2) | (298) |
The dependency pairs are split into 1 component.
take#(mark(X1),X2) | → | take#(X1,X2) | (257) |
take#(active(X1),X2) | → | take#(X1,X2) | (158) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 39603 |
[isNatList(x1)] | = | 39602 |
[U11(x1)] | = | x1 + 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 37887 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | x1 + 0 |
[U42(x1)] | = | 39603 |
[U91(x1,...,x4)] | = | x2 + 62173 |
[take(x1, x2)] | = | x1 + 24284 |
[U71(x1, x2, x3)] | = | x3 + 63548 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | x1 + 1696 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x4 + 22580 |
[U72(x1, x2)] | = | x2 + 63550 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 6371 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 68568 |
[U62(x1)] | = | x1 + 37914 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | 39601 |
[U52(x1)] | = | x1 + 8 |
[U61(x1, x2)] | = | x1 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | 1698 |
[U92(x1,...,x4)] | = | x1 + x3 + 22574 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 37903 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 28961 |
[tt] | = | 39605 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 3 |
[length(x1)] | = | x1 + 25643 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | 39601 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList(mark(X)) | → | isNatList(X) | (80) |
U11(mark(X)) | → | U11(X) | (60) |
isNatList(active(X)) | → | isNatList(X) | (81) |
U42(mark(X)) | → | U42(X) | (70) |
U11(active(X)) | → | U11(X) | (61) |
U42(active(X)) | → | U42(X) | (71) |
take#(mark(X1),X2) | → | take#(X1,X2) | (257) |
take#(active(X1),X2) | → | take#(X1,X2) | (158) |
The dependency pairs are split into 0 components.
U31#(mark(X)) | → | U31#(X) | (300) |
U31#(active(X)) | → | U31#(X) | (161) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 4604 |
[isNatList(x1)] | = | 12886 |
[U11(x1)] | = | 14914 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 28668 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 28745 |
[U91(x1,...,x4)] | = | x1 + x4 + 45916 |
[take(x1, x2)] | = | x2 + 30799 |
[U71(x1, x2, x3)] | = | x3 + 43959 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 28741 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 15107 |
[U72(x1, x2)] | = | x2 + 72623 |
[zeros] | = | 1 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 66449 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 30809 |
[U62(x1)] | = | 20316 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 51808 |
[U52(x1)] | = | 26625 |
[U61(x1, x2)] | = | x2 + 13178 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | x1 + 15857 |
[U92(x1,...,x4)] | = | x1 + 22857 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 43856 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 2060 |
[tt] | = | 28747 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 34931 |
[length(x1)] | = | 43957 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 28743 |
[U31#(x1)] | = | x1 + 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U31#(mark(X)) | → | U31#(X) | (300) |
U31#(active(X)) | → | U31#(X) | (161) |
The dependency pairs are split into 0 components.
U93#(X1,X2,mark(X3),X4) | → | U93#(X1,X2,X3,X4) | (335) |
U93#(X1,X2,active(X3),X4) | → | U93#(X1,X2,X3,X4) | (228) |
U93#(X1,X2,X3,active(X4)) | → | U93#(X1,X2,X3,X4) | (327) |
U93#(X1,X2,X3,mark(X4)) | → | U93#(X1,X2,X3,X4) | (325) |
U93#(active(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (295) |
U93#(X1,active(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (177) |
U93#(X1,mark(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (251) |
U93#(mark(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (247) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 2 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 32494 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + x4 + 34373 |
[take(x1, x2)] | = | x2 + 1596 |
[U71(x1, x2, x3)] | = | x3 + 90550 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | x1 + x3 + x4 + 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 32765 |
[U72(x1, x2)] | = | x2 + 90552 |
[zeros] | = | 27639 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 58062 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 2069 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 814 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | x1 + 19582 |
[U92(x1,...,x4)] | = | x1 + 33569 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 32775 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 1597 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 23683 |
[length(x1)] | = | 58060 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U93#(X1,X2,mark(X3),X4) | → | U93#(X1,X2,X3,X4) | (335) |
U93#(X1,X2,active(X3),X4) | → | U93#(X1,X2,X3,X4) | (228) |
U93#(X1,X2,X3,active(X4)) | → | U93#(X1,X2,X3,X4) | (327) |
U93#(X1,X2,X3,mark(X4)) | → | U93#(X1,X2,X3,X4) | (325) |
U93#(active(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (295) |
U93#(mark(X1),X2,X3,X4) | → | U93#(X1,X2,X3,X4) | (247) |
The dependency pairs are split into 1 component.
U93#(X1,active(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (177) |
U93#(X1,mark(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (251) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 1 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 4 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 6 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 6 |
[U91(x1,...,x4)] | = | x1 + x4 + 28277 |
[take(x1, x2)] | = | x2 + 1 |
[U71(x1, x2, x3)] | = | x3 + 45445 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 2 |
[U93#(x1,...,x4)] | = | x2 + 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 28266 |
[U72(x1, x2)] | = | x2 + 45447 |
[zeros] | = | 4923 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 68609 |
[0] | = | 45445 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 11 |
[U62(x1)] | = | 6 |
[mark(x1)] | = | x1 + 17206 |
[isNat(x1)] | = | x1 + 16414 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | x2 + 4 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 17207 |
[U31(x1)] | = | x1 + 3 |
[U92(x1,...,x4)] | = | x1 + 11873 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 28276 |
[active#(x1)] | = | 68609 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 1 |
[tt] | = | 8 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 33160 |
[length(x1)] | = | 45443 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 4 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U93#(X1,active(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (177) |
U93#(X1,mark(X2),X3,X4) | → | U93#(X1,X2,X3,X4) | (251) |
The dependency pairs are split into 0 components.
isNat#(active(X)) | → | isNat#(X) | (280) |
isNat#(mark(X)) | → | isNat#(X) | (261) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 5 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 12675 |
[isNat#(x1)] | = | x1 + 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + x4 + 35464 |
[take(x1, x2)] | = | x2 + 2 |
[U71(x1, x2, x3)] | = | x3 + 12672 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 35452 |
[U72(x1, x2)] | = | x2 + 12674 |
[zeros] | = | 16354 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 0 |
[0] | = | 3442 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 12 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 15 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | x1 + 2 |
[U92(x1,...,x4)] | = | x1 + 35458 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 35461 |
[active#(x1)] | = | 0 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 3 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 36963 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNat#(active(X)) | → | isNat#(X) | (280) |
isNat#(mark(X)) | → | isNat#(X) | (261) |
The dependency pairs are split into 0 components.
U81#(mark(X)) | → | U81#(X) | (236) |
U81#(active(X)) | → | U81#(X) | (169) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 5756 |
[isNatList(x1)] | = | 24354 |
[U11(x1)] | = | 23630 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 2439 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 24357 |
[U91(x1,...,x4)] | = | x1 + x4 + 65331 |
[take(x1, x2)] | = | x2 + 30618 |
[U71(x1, x2, x3)] | = | x3 + 15246 |
[U81#(x1)] | = | x1 + 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 24353 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 34702 |
[U72(x1, x2)] | = | x2 + 15248 |
[zeros] | = | 15351 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 0 |
[0] | = | 15246 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 30629 |
[U62(x1)] | = | 24358 |
[mark(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 69900 |
[U52(x1)] | = | 7737 |
[U61(x1, x2)] | = | x2 + 24356 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1)] | = | x1 + 1 |
[U92(x1,...,x4)] | = | x1 + 19793 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 59064 |
[active#(x1)] | = | 0 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 6267 |
[tt] | = | 24360 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 46902 |
[length(x1)] | = | 15244 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 24355 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U81#(mark(X)) | → | U81#(X) | (236) |
U81#(active(X)) | → | U81#(X) | (169) |
The dependency pairs are split into 0 components.
U11#(active(X)) | → | U11#(X) | (215) |
U11#(mark(X)) | → | U11#(X) | (284) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 2 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 4 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 7329 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 5 |
[U91(x1,...,x4)] | = | x1 + x4 + 46967 |
[take(x1, x2)] | = | x2 + 2 |
[U71(x1, x2, x3)] | = | x3 + 3862 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 1 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 46955 |
[U72(x1, x2)] | = | x2 + 7328 |
[zeros] | = | 46962 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 0 |
[0] | = | 845 |
[isNatList#(x1)] | = | 0 |
[s#(x1)] | = | 0 |
[nil] | = | 12 |
[U62(x1)] | = | 5 |
[mark(x1)] | = | x1 + 23155 |
[isNat(x1)] | = | x1 + 15 |
[U52(x1)] | = | 3 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | x1 + 0 |
[active(x1)] | = | x1 + 23156 |
[U31(x1)] | = | x1 + 5818 |
[U92(x1,...,x4)] | = | x1 + 46961 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 46964 |
[active#(x1)] | = | 0 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 3 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 40172 |
[length(x1)] | = | 1 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 3 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
U11#(active(X)) | → | U11#(X) | (215) |
U11#(mark(X)) | → | U11#(X) | (284) |
The dependency pairs are split into 0 components.
isNatList#(mark(X)) | → | isNatList#(X) | (218) |
isNatList#(active(X)) | → | isNatList#(X) | (139) |
[U72#(x1, x2)] | = | 0 |
[U21(x1)] | = | 5 |
[isNatList(x1)] | = | 1 |
[U11(x1)] | = | 1 |
[cons#(x1, x2)] | = | 0 |
[s(x1)] | = | x1 + 13135 |
[isNat#(x1)] | = | 0 |
[take#(x1, x2)] | = | 0 |
[U42(x1)] | = | 6 |
[U91(x1,...,x4)] | = | x1 + x4 + 30298 |
[take(x1, x2)] | = | x2 + 1 |
[U71(x1, x2, x3)] | = | x3 + 41426 |
[U81#(x1)] | = | 0 |
[U92#(x1,...,x4)] | = | 0 |
[isNatIList(x1)] | = | 2 |
[U93#(x1,...,x4)] | = | 0 |
[U93(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 30287 |
[U72(x1, x2)] | = | x2 + 54557 |
[zeros] | = | 30295 |
[U52#(x1)] | = | 0 |
[U42#(x1)] | = | 0 |
[U62#(x1)] | = | 0 |
[mark#(x1)] | = | 0 |
[0] | = | 55436 |
[isNatList#(x1)] | = | x1 + 0 |
[s#(x1)] | = | 0 |
[nil] | = | 11 |
[U62(x1)] | = | 6 |
[mark(x1)] | = | x1 + 5367 |
[isNat(x1)] | = | x1 + 16 |
[U52(x1)] | = | 2 |
[U61(x1, x2)] | = | x2 + 3 |
[U51#(x1, x2)] | = | 0 |
[U11#(x1)] | = | 0 |
[active(x1)] | = | x1 + 5368 |
[U31(x1)] | = | x1 + 3 |
[U92(x1,...,x4)] | = | x1 + 30292 |
[U41#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | 30297 |
[active#(x1)] | = | 0 |
[isNatIList#(x1)] | = | 0 |
[U21#(x1)] | = | 0 |
[U81(x1)] | = | x1 + 1 |
[tt] | = | 8 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2)] | = | x1 + x2 + 24126 |
[length(x1)] | = | 41424 |
[length#(x1)] | = | 0 |
[U41(x1, x2)] | = | x2 + 4 |
[U31#(x1)] | = | 0 |
[U91#(x1,...,x4)] | = | 0 |
[U61#(x1, x2)] | = | 0 |
isNatList#(mark(X)) | → | isNatList#(X) | (218) |
isNatList#(active(X)) | → | isNatList#(X) | (139) |
The dependency pairs are split into 0 components.