The rewrite relation of the following TRS is considered.
There are 177 ruless (increase limit for explicit display).
There are 196 ruless (increase limit for explicit display).
The dependency pairs are split into 3 components.
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (372) |
mark#(U131(X1,X2,X3,X4)) | → | mark#(X1) | (279) |
mark#(U122(X)) | → | mark#(X) | (277) |
mark#(U12(X1,X2)) | → | mark#(X1) | (369) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (274) |
mark#(U132(X1,X2,X3,X4)) | → | a__U132#(mark(X1),X2,X3,X4) | (272) |
mark#(U22(X1,X2)) | → | mark#(X1) | (273) |
mark#(U134(X1,X2,X3,X4)) | → | a__U134#(mark(X1),X2,X3,X4) | (266) |
mark#(U136(X1,X2,X3,X4)) | → | mark#(X1) | (263) |
a__U133#(tt,IL,M,N) | → | a__U134#(a__isNatKind(M),IL,M,N) | (262) |
mark#(U133(X1,X2,X3,X4)) | → | a__U133#(mark(X1),X2,X3,X4) | (261) |
a__take#(s(M),cons(N,IL)) | → | a__U131#(a__isNatIList(IL),IL,M,N) | (260) |
mark#(length(X)) | → | a__length#(mark(X)) | (357) |
a__U131#(tt,IL,M,N) | → | a__U132#(a__isNatIListKind(IL),IL,M,N) | (355) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (257) |
a__U132#(tt,IL,M,N) | → | a__U133#(a__isNat(M),IL,M,N) | (354) |
mark#(U136(X1,X2,X3,X4)) | → | a__U136#(mark(X1),X2,X3,X4) | (255) |
mark#(U52(X)) | → | mark#(X) | (349) |
a__U113#(tt,L,N) | → | a__U114#(a__isNatKind(N),L) | (250) |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (348) |
mark#(U134(X1,X2,X3,X4)) | → | mark#(X1) | (249) |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (245) |
mark#(U113(X1,X2,X3)) | → | a__U113#(mark(X1),X2,X3) | (246) |
mark#(U21(X1,X2)) | → | mark#(X1) | (247) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (244) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (344) |
a__U112#(tt,L,N) | → | a__U113#(a__isNat(N),L,N) | (343) |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (342) |
mark#(U112(X1,X2,X3)) | → | a__U112#(mark(X1),X2,X3) | (339) |
a__U114#(tt,L) | → | mark#(L) | (338) |
mark#(U33(X)) | → | mark#(X) | (240) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (337) |
mark#(U114(X1,X2)) | → | mark#(X1) | (239) |
mark#(U132(X1,X2,X3,X4)) | → | mark#(X1) | (334) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (332) |
a__U135#(tt,IL,M,N) | → | a__U136#(a__isNatKind(N),IL,M,N) | (333) |
mark#(U131(X1,X2,X3,X4)) | → | a__U131#(mark(X1),X2,X3,X4) | (235) |
mark#(U111(X1,X2,X3)) | → | mark#(X1) | (331) |
mark#(U133(X1,X2,X3,X4)) | → | mark#(X1) | (327) |
mark#(take(X1,X2)) | → | mark#(X1) | (328) |
mark#(U11(X1,X2)) | → | mark#(X1) | (233) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (326) |
mark#(U113(X1,X2,X3)) | → | mark#(X1) | (228) |
mark#(U121(X1,X2)) | → | mark#(X1) | (222) |
mark#(cons(X1,X2)) | → | mark#(X1) | (318) |
mark#(U45(X1,X2)) | → | mark#(X1) | (221) |
mark#(U135(X1,X2,X3,X4)) | → | a__U135#(mark(X1),X2,X3,X4) | (317) |
a__U136#(tt,IL,M,N) | → | mark#(N) | (219) |
mark#(U135(X1,X2,X3,X4)) | → | mark#(X1) | (214) |
mark#(U61(X1,X2)) | → | mark#(X1) | (213) |
mark#(U32(X1,X2)) | → | mark#(X1) | (310) |
mark#(U62(X)) | → | mark#(X) | (210) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (309) |
mark#(U106(X)) | → | mark#(X) | (208) |
mark#(U81(X)) | → | mark#(X) | (206) |
a__length#(cons(N,L)) | → | a__U111#(a__isNatList(L),L,N) | (205) |
a__U134#(tt,IL,M,N) | → | a__U135#(a__isNat(N),IL,M,N) | (307) |
mark#(U13(X)) | → | mark#(X) | (202) |
mark#(U31(X1,X2)) | → | mark#(X1) | (305) |
mark#(U111(X1,X2,X3)) | → | a__U111#(mark(X1),X2,X3) | (200) |
mark#(U46(X)) | → | mark#(X) | (303) |
mark#(U23(X)) | → | mark#(X) | (198) |
mark#(U105(X1,X2)) | → | mark#(X1) | (302) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (299) |
a__U114#(tt,L) | → | a__length#(mark(L)) | (194) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (292) |
mark#(U71(X)) | → | mark#(X) | (187) |
mark#(U114(X1,X2)) | → | a__U114#(mark(X1),X2) | (290) |
mark#(U96(X)) | → | mark#(X) | (289) |
mark#(length(X)) | → | mark#(X) | (288) |
mark#(s(X)) | → | mark#(X) | (287) |
mark#(U95(X1,X2)) | → | mark#(X1) | (285) |
mark#(U51(X1,X2)) | → | mark#(X1) | (283) |
mark#(U112(X1,X2,X3)) | → | mark#(X1) | (179) |
mark#(take(X1,X2)) | → | mark#(X2) | (281) |
[a__U94#(x1, x2, x3)] | = | 0 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 24635 |
[a__U131#(x1,...,x4)] | = | x1 + x2 + x4 + 56408 |
[U21(x1, x2)] | = | x1 + 0 |
[a__U102(x1, x2, x3)] | = | x1 + 0 |
[a__U45(x1, x2)] | = | x1 + 0 |
[isNatList(x1)] | = | 24635 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x1 + 0 |
[a__U92#(x1, x2, x3)] | = | 0 |
[a__U104(x1, x2, x3)] | = | x1 + 0 |
[U136(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U112#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[s(x1)] | = | x1 + 0 |
[a__U133#(x1,...,x4)] | = | x4 + 56408 |
[U105(x1, x2)] | = | x1 + 0 |
[a__U31#(x1, x2)] | = | 0 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | 0 |
[a__U114(x1, x2)] | = | x1 + x2 + 8922 |
[a__isNatIList(x1)] | = | 24635 |
[a__U33(x1)] | = | x1 + 0 |
[U106(x1)] | = | x1 + 0 |
[a__isNatIListKind#(x1)] | = | 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x1 + 0 |
[U42(x1, x2, x3)] | = | x1 + 0 |
[U91(x1, x2, x3)] | = | x1 + 0 |
[a__isNat#(x1)] | = | 0 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | x4 + 24635 |
[take(x1, x2)] | = | x1 + x2 + 56410 |
[U71(x1)] | = | x1 + 0 |
[a__U62(x1)] | = | x1 + 0 |
[a__U44(x1, x2, x3)] | = | x1 + 0 |
[U131(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[isNatIList(x1)] | = | 24635 |
[U135(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[U101(x1, x2, x3)] | = | x1 + 0 |
[a__U43#(x1, x2, x3)] | = | 0 |
[U95(x1, x2)] | = | x1 + 0 |
[U111(x1, x2, x3)] | = | x1 + x2 + x3 + 8922 |
[U132(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[U43(x1, x2, x3)] | = | x1 + 0 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x1 + 12267 |
[a__U135#(x1,...,x4)] | = | x4 + 24636 |
[a__U44#(x1, x2, x3)] | = | 0 |
[U103(x1, x2, x3)] | = | x1 + 0 |
[a__U111(x1, x2, x3)] | = | x1 + x2 + x3 + 8922 |
[a__U103#(x1, x2, x3)] | = | 0 |
[U44(x1, x2, x3)] | = | x1 + 0 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | x2 + 24635 |
[a__U51#(x1, x2)] | = | 0 |
[U23(x1)] | = | x1 + 0 |
[a__U22(x1, x2)] | = | x1 + 0 |
[U93(x1, x2, x3)] | = | x1 + 0 |
[a__U94(x1, x2, x3)] | = | x1 + 0 |
[a__U106(x1)] | = | x1 + 0 |
[a__U11#(x1, x2)] | = | 0 |
[U94(x1, x2, x3)] | = | x1 + 0 |
[zeros] | = | 1 |
[a__U31(x1, x2)] | = | x1 + 0 |
[a__U51(x1, x2)] | = | x1 + 0 |
[a__U81(x1)] | = | x1 + 0 |
[a__take#(x1, x2)] | = | x2 + 81043 |
[U12(x1, x2)] | = | x1 + 0 |
[a__isNatList(x1)] | = | 24635 |
[a__U43(x1, x2, x3)] | = | x1 + 0 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U42#(x1, x2, x3)] | = | 0 |
[a__U41(x1, x2, x3)] | = | x1 + 0 |
[a__U134(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | 0 |
[U104(x1, x2, x3)] | = | x1 + 0 |
[a__U122(x1)] | = | x1 + 5037 |
[a__U21#(x1, x2)] | = | 0 |
[a__isNatIList#(x1)] | = | 0 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[U113(x1, x2, x3)] | = | x1 + x2 + x3 + 8922 |
[mark#(x1)] | = | x1 + 24634 |
[0] | = | 0 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | x2 + x3 + 24635 |
[U134(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U21(x1, x2)] | = | x1 + 0 |
[a__U32(x1, x2)] | = | x1 + 0 |
[a__U91(x1, x2, x3)] | = | x1 + 0 |
[a__U111#(x1, x2, x3)] | = | x2 + x3 + 24635 |
[nil] | = | 1 |
[isNatIListKind(x1)] | = | 24635 |
[U114(x1, x2)] | = | x1 + x2 + 8922 |
[U62(x1)] | = | x1 + 0 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | 0 |
[U45(x1, x2)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 0 |
[U133(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U101#(x1, x2, x3)] | = | 0 |
[a__U11(x1, x2)] | = | x1 + 0 |
[U32(x1, x2)] | = | x1 + 0 |
[a__U42(x1, x2, x3)] | = | x1 + 0 |
[a__U93(x1, x2, x3)] | = | x1 + 0 |
[U33(x1)] | = | x1 + 0 |
[a__U45#(x1, x2)] | = | 0 |
[a__U52(x1)] | = | x1 + 0 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__length#(x1)] | = | x1 + 24635 |
[a__U105#(x1, x2)] | = | 0 |
[a__U12(x1, x2)] | = | x1 + 0 |
[a__isNatIListKind(x1)] | = | 24635 |
[a__U104#(x1, x2, x3)] | = | 0 |
[isNat(x1)] | = | 24635 |
[U46(x1)] | = | x1 + 0 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | x1 + 0 |
[U61(x1, x2)] | = | x1 + 0 |
[a__U46(x1)] | = | x1 + 0 |
[a__U22#(x1, x2)] | = | 0 |
[a__U113(x1, x2, x3)] | = | x1 + x2 + x3 + 8922 |
[U96(x1)] | = | x1 + 0 |
[a__U13(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x1 + 0 |
[a__isNatList#(x1)] | = | 0 |
[a__U71(x1)] | = | x1 + 0 |
[U92(x1, x2, x3)] | = | x1 + 0 |
[U112(x1, x2, x3)] | = | x1 + x2 + x3 + 8922 |
[cons(x1, x2)] | = | x1 + x2 + 0 |
[a__U92(x1, x2, x3)] | = | x1 + 0 |
[a__U61(x1, x2)] | = | x1 + 0 |
[U102(x1, x2, x3)] | = | x1 + 0 |
[a__U105(x1, x2)] | = | x1 + 0 |
[a__take(x1, x2)] | = | x1 + x2 + 56410 |
[U81(x1)] | = | x1 + 0 |
[a__U95#(x1, x2)] | = | 0 |
[a__U41#(x1, x2, x3)] | = | 0 |
[tt] | = | 24635 |
[a__U131(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__isNat(x1)] | = | 24635 |
[U13(x1)] | = | x1 + 0 |
[a__U133(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 31775 |
[a__U23(x1)] | = | x1 + 0 |
[a__U96(x1)] | = | x1 + 0 |
[a__isNatKind(x1)] | = | 24635 |
[a__U134#(x1,...,x4)] | = | x4 + 56407 |
[U22(x1, x2)] | = | x1 + 0 |
[U51(x1, x2)] | = | x1 + 0 |
[a__U132#(x1,...,x4)] | = | x2 + x4 + 56409 |
[a__U103(x1, x2, x3)] | = | x1 + 0 |
[length(x1)] | = | x1 + 33557 |
[a__U112(x1, x2, x3)] | = | x1 + x2 + x3 + 8922 |
[U41(x1, x2, x3)] | = | x1 + 0 |
[a__U32#(x1, x2)] | = | 0 |
[a__zeros] | = | 1 |
[a__U101(x1, x2, x3)] | = | x1 + 0 |
[a__U91#(x1, x2, x3)] | = | 0 |
[U121(x1, x2)] | = | x1 + 12267 |
[a__length(x1)] | = | x1 + 33557 |
[U122(x1)] | = | x1 + 5037 |
There are 177 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsmark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (372) |
mark#(U131(X1,X2,X3,X4)) | → | mark#(X1) | (279) |
mark#(U122(X)) | → | mark#(X) | (277) |
mark#(U134(X1,X2,X3,X4)) | → | a__U134#(mark(X1),X2,X3,X4) | (266) |
mark#(U136(X1,X2,X3,X4)) | → | mark#(X1) | (263) |
a__U133#(tt,IL,M,N) | → | a__U134#(a__isNatKind(M),IL,M,N) | (262) |
mark#(U133(X1,X2,X3,X4)) | → | a__U133#(mark(X1),X2,X3,X4) | (261) |
mark#(length(X)) | → | a__length#(mark(X)) | (357) |
a__U131#(tt,IL,M,N) | → | a__U132#(a__isNatIListKind(IL),IL,M,N) | (355) |
a__U132#(tt,IL,M,N) | → | a__U133#(a__isNat(M),IL,M,N) | (354) |
mark#(U136(X1,X2,X3,X4)) | → | a__U136#(mark(X1),X2,X3,X4) | (255) |
mark#(U134(X1,X2,X3,X4)) | → | mark#(X1) | (249) |
mark#(U113(X1,X2,X3)) | → | a__U113#(mark(X1),X2,X3) | (246) |
mark#(U112(X1,X2,X3)) | → | a__U112#(mark(X1),X2,X3) | (339) |
a__U114#(tt,L) | → | mark#(L) | (338) |
mark#(U114(X1,X2)) | → | mark#(X1) | (239) |
mark#(U132(X1,X2,X3,X4)) | → | mark#(X1) | (334) |
a__U135#(tt,IL,M,N) | → | a__U136#(a__isNatKind(N),IL,M,N) | (333) |
mark#(U131(X1,X2,X3,X4)) | → | a__U131#(mark(X1),X2,X3,X4) | (235) |
mark#(U111(X1,X2,X3)) | → | mark#(X1) | (331) |
mark#(U133(X1,X2,X3,X4)) | → | mark#(X1) | (327) |
mark#(take(X1,X2)) | → | mark#(X1) | (328) |
mark#(U113(X1,X2,X3)) | → | mark#(X1) | (228) |
mark#(U121(X1,X2)) | → | mark#(X1) | (222) |
mark#(U135(X1,X2,X3,X4)) | → | a__U135#(mark(X1),X2,X3,X4) | (317) |
a__U136#(tt,IL,M,N) | → | mark#(N) | (219) |
mark#(U135(X1,X2,X3,X4)) | → | mark#(X1) | (214) |
a__U134#(tt,IL,M,N) | → | a__U135#(a__isNat(N),IL,M,N) | (307) |
mark#(U111(X1,X2,X3)) | → | a__U111#(mark(X1),X2,X3) | (200) |
mark#(U114(X1,X2)) | → | a__U114#(mark(X1),X2) | (290) |
mark#(length(X)) | → | mark#(X) | (288) |
mark#(U112(X1,X2,X3)) | → | mark#(X1) | (179) |
mark#(take(X1,X2)) | → | mark#(X2) | (281) |
The dependency pairs are split into 2 components.
a__length#(cons(N,L)) | → | a__U111#(a__isNatList(L),L,N) | (205) |
a__U112#(tt,L,N) | → | a__U113#(a__isNat(N),L,N) | (343) |
a__U114#(tt,L) | → | a__length#(mark(L)) | (194) |
a__U113#(tt,L,N) | → | a__U114#(a__isNatKind(N),L) | (250) |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (342) |
[a__U94#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__isNatKind#(x1)] | = |
|
||||||||||||||||||||||||||
[isNatKind(x1)] | = |
|
||||||||||||||||||||||||||
[a__U131#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U21(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U102(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U45(x1, x2)] | = |
|
||||||||||||||||||||||||||
[isNatList(x1)] | = |
|
||||||||||||||||||||||||||
[a__U71#(x1)] | = |
|
||||||||||||||||||||||||||
[U11(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U92#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U104(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U136(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U112#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[s(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[a__U133#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U105(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U31#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U132(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U33#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U93#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U114(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__isNatIList(x1)] | = |
|
||||||||||||||||||||||||||
[a__U33(x1)] | = |
|
||||||||||||||||||||||||||
[U106(x1)] | = |
|
||||||||||||||||||||||||||
[a__isNatIListKind#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U23#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U95(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U42(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U91(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__isNat#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U106#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U136#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[take(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U71(x1)] | = |
|
||||||||||||||||||||||||||
[a__U62(x1)] | = |
|
||||||||||||||||||||||||||
[a__U44(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U131(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||||||||||||||||
[U135(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U101(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U43#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U95(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U111(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U132(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U43(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U13#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U121(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U135#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U44#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U103(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U111(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U103#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U44(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U46#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U114#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U51#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U23(x1)] | = |
|
||||||||||||||||||||||||||
[a__U22(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U93(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U94(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U106(x1)] | = |
|
||||||||||||||||||||||||||
[a__U11#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U94(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||
[a__U31(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U51(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U81(x1)] | = |
|
||||||||||||||||||||||||||
[a__take#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U12(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__isNatList(x1)] | = |
|
||||||||||||||||||||||||||
[a__U43(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U62#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U136(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U42#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U41(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U134(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U122#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U12#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U104(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U122(x1)] | = |
x1 +
|
||||||||||||||||||||||||||
[a__U21#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__isNatIList#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U81#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U61#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U113(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[mark#(x1)] | = |
|
||||||||||||||||||||||||||
[0] | = |
|
||||||||||||||||||||||||||
[a__zeros#] | = |
|
||||||||||||||||||||||||||
[a__U113#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U134(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U21(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U32(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U91(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U111#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||
[isNatIListKind(x1)] | = |
|
||||||||||||||||||||||||||
[U114(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U62(x1)] | = |
|
||||||||||||||||||||||||||
[a__U52#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U102#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U45(x1, x2)] | = |
|
||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||
[U133(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U101#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U11(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U32(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U42(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U93(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U33(x1)] | = |
|
||||||||||||||||||||||||||
[a__U45#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U52(x1)] | = |
|
||||||||||||||||||||||||||
[a__U96#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U135(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__length#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U105#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U12(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__isNatIListKind(x1)] | = |
|
||||||||||||||||||||||||||
[a__U104#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[isNat(x1)] | = |
|
||||||||||||||||||||||||||
[U46(x1)] | = |
|
||||||||||||||||||||||||||
[a__U121#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U52(x1)] | = |
|
||||||||||||||||||||||||||
[U61(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U46(x1)] | = |
|
||||||||||||||||||||||||||
[a__U22#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U113(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U96(x1)] | = |
|
||||||||||||||||||||||||||
[a__U13(x1)] | = |
|
||||||||||||||||||||||||||
[U31(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__isNatList#(x1)] | = |
|
||||||||||||||||||||||||||
[a__U71(x1)] | = |
|
||||||||||||||||||||||||||
[U92(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U112(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[cons(x1, x2)] | = |
x1 +
|
||||||||||||||||||||||||||
[a__U92(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U61(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U102(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U105(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__take(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U81(x1)] | = |
|
||||||||||||||||||||||||||
[a__U95#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U41#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||
[a__U131(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__isNat(x1)] | = |
|
||||||||||||||||||||||||||
[U13(x1)] | = |
|
||||||||||||||||||||||||||
[a__U133(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U23(x1)] | = |
|
||||||||||||||||||||||||||
[a__U96(x1)] | = |
|
||||||||||||||||||||||||||
[a__isNatKind(x1)] | = |
|
||||||||||||||||||||||||||
[a__U134#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[U22(x1, x2)] | = |
|
||||||||||||||||||||||||||
[U51(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__U132#(x1,...,x4)] | = |
|
||||||||||||||||||||||||||
[a__U103(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[length(x1)] | = |
|
||||||||||||||||||||||||||
[a__U112(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U41(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U32#(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__zeros] | = |
|
||||||||||||||||||||||||||
[a__U101(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[a__U91#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||
[U121(x1, x2)] | = |
|
||||||||||||||||||||||||||
[a__length(x1)] | = |
|
||||||||||||||||||||||||||
[U122(x1)] | = |
|
There are 177 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsa__length#(cons(N,L)) | → | a__U111#(a__isNatList(L),L,N) | (205) |
a__U112#(tt,L,N) | → | a__U113#(a__isNat(N),L,N) | (343) |
a__U114#(tt,L) | → | a__length#(mark(L)) | (194) |
a__U113#(tt,L,N) | → | a__U114#(a__isNatKind(N),L) | (250) |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (342) |
The dependency pairs are split into 0 components.
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (245) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (332) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (299) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (292) |
mark#(U13(X)) | → | mark#(X) | (202) |
mark#(U32(X1,X2)) | → | mark#(X1) | (310) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (244) |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (348) |
mark#(cons(X1,X2)) | → | mark#(X1) | (318) |
mark#(U96(X)) | → | mark#(X) | (289) |
mark#(U51(X1,X2)) | → | mark#(X1) | (283) |
mark#(U45(X1,X2)) | → | mark#(X1) | (221) |
mark#(U62(X)) | → | mark#(X) | (210) |
mark#(U12(X1,X2)) | → | mark#(X1) | (369) |
mark#(U33(X)) | → | mark#(X) | (240) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (257) |
mark#(U21(X1,X2)) | → | mark#(X1) | (247) |
mark#(U11(X1,X2)) | → | mark#(X1) | (233) |
mark#(U95(X1,X2)) | → | mark#(X1) | (285) |
mark#(U52(X)) | → | mark#(X) | (349) |
mark#(U106(X)) | → | mark#(X) | (208) |
mark#(U23(X)) | → | mark#(X) | (198) |
mark#(U46(X)) | → | mark#(X) | (303) |
mark#(U61(X1,X2)) | → | mark#(X1) | (213) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (274) |
mark#(U81(X)) | → | mark#(X) | (206) |
mark#(U105(X1,X2)) | → | mark#(X1) | (302) |
mark#(U71(X)) | → | mark#(X) | (187) |
mark#(s(X)) | → | mark#(X) | (287) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (344) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (309) |
mark#(U22(X1,X2)) | → | mark#(X1) | (273) |
mark#(U31(X1,X2)) | → | mark#(X1) | (305) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (337) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (326) |
[a__U94#(x1, x2, x3)] | = | 0 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | x1 + 4 |
[a__U131#(x1,...,x4)] | = | 56408 |
[U21(x1, x2)] | = | x1 + 5 |
[a__U102(x1, x2, x3)] | = | x2 + x3 + 7 |
[a__U45(x1, x2)] | = | x1 + x2 + 32 |
[isNatList(x1)] | = | 3 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x1 + 4 |
[a__U92#(x1, x2, x3)] | = | 0 |
[a__U104(x1, x2, x3)] | = | x1 + x3 + 10 |
[U136(x1,...,x4)] | = | x1 + x4 + 31775 |
[a__U112#(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 8945 |
[a__U133#(x1,...,x4)] | = | 56408 |
[U105(x1, x2)] | = | x1 + 24633 |
[a__U31#(x1, x2)] | = | 0 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x4 + 5 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | 0 |
[a__U114(x1, x2)] | = | x2 + 8943 |
[a__isNatIList(x1)] | = | x1 + 2 |
[a__U33(x1)] | = | 8 |
[U106(x1)] | = | x1 + 16 |
[a__isNatIListKind#(x1)] | = | 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x1 + 11 |
[U42(x1, x2, x3)] | = | x1 + 25 |
[U91(x1, x2, x3)] | = | x1 + 4 |
[a__isNat#(x1)] | = | 0 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | 24635 |
[take(x1, x2)] | = | x1 + x2 + 56410 |
[U71(x1)] | = | x1 + 3 |
[a__U62(x1)] | = | x1 + 2 |
[a__U44(x1, x2, x3)] | = | x2 + 33 |
[U131(x1,...,x4)] | = | 2 |
[isNatIList(x1)] | = | 3 |
[U135(x1,...,x4)] | = | x1 + x3 + 13 |
[U101(x1, x2, x3)] | = | x1 + 2 |
[a__U43#(x1, x2, x3)] | = | 0 |
[U95(x1, x2)] | = | x1 + 12 |
[U111(x1, x2, x3)] | = | x1 + x2 + 8941 |
[U132(x1,...,x4)] | = | x3 + 31779 |
[U43(x1, x2, x3)] | = | x1 + x2 + 28 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x1 + 1 |
[a__U135#(x1,...,x4)] | = | 24636 |
[a__U44#(x1, x2, x3)] | = | 0 |
[U103(x1, x2, x3)] | = | x1 + x2 + x3 + 7 |
[a__U111(x1, x2, x3)] | = | x3 + 8940 |
[a__U103#(x1, x2, x3)] | = | 0 |
[U44(x1, x2, x3)] | = | x1 + x3 + 34 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | 1 |
[a__U51#(x1, x2)] | = | 0 |
[U23(x1)] | = | x1 + 10 |
[a__U22(x1, x2)] | = | x2 + 10 |
[U93(x1, x2, x3)] | = | x1 + x3 + 6 |
[a__U94(x1, x2, x3)] | = | x1 + x2 + x3 + 9 |
[a__U106(x1)] | = | x1 + 15 |
[a__U11#(x1, x2)] | = | 0 |
[U94(x1, x2, x3)] | = | x1 + 10 |
[zeros] | = | 0 |
[a__U31(x1, x2)] | = | x1 + 1 |
[a__U51(x1, x2)] | = | x2 + 3 |
[a__U81(x1)] | = | 4 |
[a__take#(x1, x2)] | = | 81043 |
[U12(x1, x2)] | = | x1 + 8 |
[a__isNatList(x1)] | = | 2 |
[a__U43(x1, x2, x3)] | = | x1 + x3 + 27 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x1 + x2 + x3 + 15 |
[a__U42#(x1, x2, x3)] | = | 0 |
[a__U41(x1, x2, x3)] | = | 23 |
[a__U134(x1,...,x4)] | = | x1 + x2 + x3 + x4 + 10 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | 0 |
[U104(x1, x2, x3)] | = | x1 + 11 |
[a__U122(x1)] | = | 7 |
[a__U21#(x1, x2)] | = | 0 |
[a__isNatIList#(x1)] | = | 0 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[U113(x1, x2, x3)] | = | x2 + 8943 |
[mark#(x1)] | = | x1 + 24634 |
[0] | = | 3481 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | 1 |
[U134(x1,...,x4)] | = | x1 + 11 |
[a__U21(x1, x2)] | = | x1 + x2 + 4 |
[a__U32(x1, x2)] | = | x2 + 7 |
[a__U91(x1, x2, x3)] | = | x2 + x3 + 3 |
[a__U111#(x1, x2, x3)] | = | 0 |
[nil] | = | 8 |
[isNatIListKind(x1)] | = | 3 |
[U114(x1, x2)] | = | x1 + 8944 |
[U62(x1)] | = | x1 + 3 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | 0 |
[U45(x1, x2)] | = | x1 + 33 |
[mark(x1)] | = | 1 |
[U133(x1,...,x4)] | = | x1 + x3 + 31778 |
[a__U101#(x1, x2, x3)] | = | 0 |
[a__U11(x1, x2)] | = | x1 + x2 + 3 |
[U32(x1, x2)] | = | x1 + 8 |
[a__U42(x1, x2, x3)] | = | x2 + 24 |
[a__U93(x1, x2, x3)] | = | x1 + 5 |
[U33(x1)] | = | x1 + 9 |
[a__U45#(x1, x2)] | = | 0 |
[a__U52(x1)] | = | 4 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x1 + x4 + 12 |
[a__length#(x1)] | = | 1 |
[a__U105#(x1, x2)] | = | 0 |
[a__U12(x1, x2)] | = | x1 + x2 + 7 |
[a__isNatIListKind(x1)] | = | 2 |
[a__U104#(x1, x2, x3)] | = | 0 |
[isNat(x1)] | = | 5 |
[U46(x1)] | = | x1 + 3 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | x1 + 5 |
[U61(x1, x2)] | = | x1 + x2 + 4 |
[a__U46(x1)] | = | 2 |
[a__U22#(x1, x2)] | = | 0 |
[a__U113(x1, x2, x3)] | = | x3 + 8942 |
[U96(x1)] | = | x1 + 18 |
[a__U13(x1)] | = | 13 |
[U31(x1, x2)] | = | x1 + 2 |
[a__isNatList#(x1)] | = | 0 |
[a__U71(x1)] | = | x1 + 2 |
[U92(x1, x2, x3)] | = | x1 + x2 + 2 |
[U112(x1, x2, x3)] | = | x1 + x2 + x3 + 8942 |
[cons(x1, x2)] | = | x1 + 20 |
[a__U92(x1, x2, x3)] | = | x1 + 1 |
[a__U61(x1, x2)] | = | 3 |
[U102(x1, x2, x3)] | = | x1 + 8 |
[a__U105(x1, x2)] | = | 16 |
[a__take(x1, x2)] | = | 2 |
[U81(x1)] | = | x1 + 5 |
[a__U95#(x1, x2)] | = | 0 |
[a__U41#(x1, x2, x3)] | = | 0 |
[tt] | = | 5 |
[a__U131(x1,...,x4)] | = | x1 + x3 + x4 + 1 |
[a__isNat(x1)] | = | 4 |
[U13(x1)] | = | x1 + 14 |
[a__U133(x1,...,x4)] | = | x1 + x4 + 7 |
[a__U23(x1)] | = | x1 + 9 |
[a__U96(x1)] | = | 17 |
[a__isNatKind(x1)] | = | 3 |
[a__U134#(x1,...,x4)] | = | 56407 |
[U22(x1, x2)] | = | x1 + 11 |
[U51(x1, x2)] | = | x1 + 4 |
[a__U132#(x1,...,x4)] | = | 56409 |
[a__U103(x1, x2, x3)] | = | x1 + 6 |
[length(x1)] | = | 3473 |
[a__U112(x1, x2, x3)] | = | 8941 |
[U41(x1, x2, x3)] | = | x1 + x2 + x3 + 24 |
[a__U32#(x1, x2)] | = | 0 |
[a__zeros] | = | 2 |
[a__U101(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U91#(x1, x2, x3)] | = | 0 |
[U121(x1, x2)] | = | x1 + x2 + 12267 |
[a__length(x1)] | = | x1 + 3472 |
[U122(x1)] | = | 8 |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (245) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (332) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (299) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (292) |
mark#(U13(X)) | → | mark#(X) | (202) |
mark#(U32(X1,X2)) | → | mark#(X1) | (310) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (244) |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (348) |
mark#(cons(X1,X2)) | → | mark#(X1) | (318) |
mark#(U96(X)) | → | mark#(X) | (289) |
mark#(U51(X1,X2)) | → | mark#(X1) | (283) |
mark#(U45(X1,X2)) | → | mark#(X1) | (221) |
mark#(U62(X)) | → | mark#(X) | (210) |
mark#(U12(X1,X2)) | → | mark#(X1) | (369) |
mark#(U33(X)) | → | mark#(X) | (240) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (257) |
mark#(U21(X1,X2)) | → | mark#(X1) | (247) |
mark#(U11(X1,X2)) | → | mark#(X1) | (233) |
mark#(U95(X1,X2)) | → | mark#(X1) | (285) |
mark#(U52(X)) | → | mark#(X) | (349) |
mark#(U106(X)) | → | mark#(X) | (208) |
mark#(U23(X)) | → | mark#(X) | (198) |
mark#(U46(X)) | → | mark#(X) | (303) |
mark#(U61(X1,X2)) | → | mark#(X1) | (213) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (274) |
mark#(U81(X)) | → | mark#(X) | (206) |
mark#(U105(X1,X2)) | → | mark#(X1) | (302) |
mark#(U71(X)) | → | mark#(X) | (187) |
mark#(s(X)) | → | mark#(X) | (287) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (344) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (309) |
mark#(U22(X1,X2)) | → | mark#(X1) | (273) |
mark#(U31(X1,X2)) | → | mark#(X1) | (305) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (337) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (326) |
The dependency pairs are split into 0 components.
a__isNatList#(cons(V1,V2)) | → | a__U91#(a__isNatKind(V1),V1,V2) | (275) |
a__U93#(tt,V1,V2) | → | a__U94#(a__isNatIListKind(V2),V1,V2) | (367) |
a__U92#(tt,V1,V2) | → | a__U93#(a__isNatIListKind(V2),V1,V2) | (269) |
a__U104#(tt,V1,V2) | → | a__U105#(a__isNat(V1),V2) | (363) |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (360) |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (259) |
a__U31#(tt,V) | → | a__U32#(a__isNatIListKind(V),V) | (358) |
a__U105#(tt,V2) | → | a__isNatIList#(V2) | (353) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (253) |
a__U101#(tt,V1,V2) | → | a__U102#(a__isNatKind(V1),V1,V2) | (350) |
a__U91#(tt,V1,V2) | → | a__U92#(a__isNatKind(V1),V1,V2) | (345) |
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (340) |
a__U104#(tt,V1,V2) | → | a__isNat#(V1) | (234) |
a__U12#(tt,V1) | → | a__isNatList#(V1) | (231) |
a__isNatList#(take(V1,V2)) | → | a__U101#(a__isNatKind(V1),V1,V2) | (324) |
a__isNatIList#(V) | → | a__U31#(a__isNatIListKind(V),V) | (227) |
a__U103#(tt,V1,V2) | → | a__U104#(a__isNatIListKind(V2),V1,V2) | (321) |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (223) |
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (319) |
a__U32#(tt,V) | → | a__isNatList#(V) | (315) |
a__U102#(tt,V1,V2) | → | a__U103#(a__isNatIListKind(V2),V1,V2) | (209) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (207) |
a__U94#(tt,V1,V2) | → | a__U95#(a__isNat(V1),V2) | (204) |
a__U94#(tt,V1,V2) | → | a__isNat#(V1) | (304) |
a__U44#(tt,V1,V2) | → | a__isNat#(V1) | (195) |
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (298) |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (192) |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (293) |
a__U95#(tt,V2) | → | a__isNatList#(V2) | (291) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (183) |
[a__U94#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 4271 |
[a__U131#(x1,...,x4)] | = | 56408 |
[U21(x1, x2)] | = | x1 + 4257 |
[a__U102(x1, x2, x3)] | = | x1 + x2 + x3 + 8502 |
[a__U45(x1, x2)] | = | x1 + x2 + 4262 |
[isNatList(x1)] | = | 8506 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x2 + 4257 |
[a__U92#(x1, x2, x3)] | = | x2 + x3 + 8512 |
[a__U104(x1, x2, x3)] | = | x2 + 8509 |
[U136(x1,...,x4)] | = | x4 + 8519 |
[a__U112#(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 0 |
[a__U133#(x1,...,x4)] | = | 56408 |
[U105(x1, x2)] | = | x1 + 8511 |
[a__U31#(x1, x2)] | = | x2 + 8514 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x3 + 2 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | x2 + x3 + 8512 |
[a__U114(x1, x2)] | = | x1 + x2 + 4246 |
[a__isNatIList(x1)] | = | x1 + 4255 |
[a__U33(x1)] | = | 8514 |
[U106(x1)] | = | 8512 |
[a__isNatIListKind#(x1)] | = | 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x2 + 8510 |
[U42(x1, x2, x3)] | = | x1 + 8515 |
[U91(x1, x2, x3)] | = | x1 + x3 + 8507 |
[a__isNat#(x1)] | = | x1 + 8512 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | 24635 |
[take(x1, x2)] | = | x1 + x2 + 4265 |
[U71(x1)] | = | 2 |
[a__U62(x1)] | = | 8512 |
[a__U44(x1, x2, x3)] | = | x3 + 8516 |
[U131(x1,...,x4)] | = | x4 + 2 |
[isNatIList(x1)] | = | 4256 |
[U135(x1,...,x4)] | = | x2 + 8518 |
[U101(x1, x2, x3)] | = | x2 + 12772 |
[a__U43#(x1, x2, x3)] | = | x2 + x3 + 8515 |
[U95(x1, x2)] | = | 8511 |
[U111(x1, x2, x3)] | = | 2 |
[U132(x1,...,x4)] | = | x1 + 3 |
[U43(x1, x2, x3)] | = | x2 + 4 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x2 + 4256 |
[a__U135#(x1,...,x4)] | = | 24636 |
[a__U44#(x1, x2, x3)] | = | x2 + x3 + 8515 |
[U103(x1, x2, x3)] | = | x2 + 17016 |
[a__U111(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U103#(x1, x2, x3)] | = | x2 + x3 + 8518 |
[U44(x1, x2, x3)] | = | x1 + 8517 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | 1 |
[a__U51#(x1, x2)] | = | 0 |
[U23(x1)] | = | x1 + 8512 |
[a__U22(x1, x2)] | = | x2 + 4257 |
[U93(x1, x2, x3)] | = | 8509 |
[a__U94(x1, x2, x3)] | = | x2 + x3 + 8509 |
[a__U106(x1)] | = | 8511 |
[a__U11#(x1, x2)] | = | x2 + 8512 |
[U94(x1, x2, x3)] | = | x3 + 8510 |
[zeros] | = | 4256 |
[a__U31(x1, x2)] | = | 4256 |
[a__U51(x1, x2)] | = | 8512 |
[a__U81(x1)] | = | 8511 |
[a__take#(x1, x2)] | = | 81043 |
[U12(x1, x2)] | = | x1 + x2 + 4258 |
[a__isNatList(x1)] | = | x1 + 8505 |
[a__U43(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x2 + 8518 |
[a__U42#(x1, x2, x3)] | = | x2 + x3 + 8515 |
[a__U41(x1, x2, x3)] | = | x1 + 1 |
[a__U134(x1,...,x4)] | = | x2 + x4 + 8516 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | x2 + 8512 |
[U104(x1, x2, x3)] | = | 8510 |
[a__U122(x1)] | = | 4257 |
[a__U21#(x1, x2)] | = | x2 + 8512 |
[a__isNatIList#(x1)] | = | x1 + 8515 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[U113(x1, x2, x3)] | = | x2 + 8516 |
[mark#(x1)] | = | 24634 |
[0] | = | 4255 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | 1 |
[U134(x1,...,x4)] | = | x1 + 8517 |
[a__U21(x1, x2)] | = | 4256 |
[a__U32(x1, x2)] | = | x1 + x2 + 1 |
[a__U91(x1, x2, x3)] | = | 8506 |
[a__U111#(x1, x2, x3)] | = | 0 |
[nil] | = | 4258 |
[isNatIListKind(x1)] | = | 1 |
[U114(x1, x2)] | = | 0 |
[U62(x1)] | = | 8512 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | x2 + x3 + 8519 |
[U45(x1, x2)] | = | 4263 |
[mark(x1)] | = | 4254 |
[U133(x1,...,x4)] | = | x2 + x3 + 8516 |
[a__U101#(x1, x2, x3)] | = | x2 + x3 + 8520 |
[a__U11(x1, x2)] | = | 4256 |
[U32(x1, x2)] | = | x1 + 17 |
[a__U42(x1, x2, x3)] | = | x2 + 8514 |
[a__U93(x1, x2, x3)] | = | x3 + 8508 |
[U33(x1)] | = | 8515 |
[a__U45#(x1, x2)] | = | x2 + 8515 |
[a__U52(x1)] | = | 8512 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x3 + x4 + 8517 |
[a__length#(x1)] | = | 1 |
[a__U105#(x1, x2)] | = | x2 + 8516 |
[a__U12(x1, x2)] | = | x2 + 4257 |
[a__isNatIListKind(x1)] | = | 8512 |
[a__U104#(x1, x2, x3)] | = | x1 + x2 + x3 + 5 |
[isNat(x1)] | = | x1 + 4256 |
[U46(x1)] | = | x1 + 4256 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | 8512 |
[U61(x1, x2)] | = | 8512 |
[a__U46(x1)] | = | 4255 |
[a__U22#(x1, x2)] | = | x2 + 8512 |
[a__U113(x1, x2, x3)] | = | x3 + 8515 |
[U96(x1)] | = | x1 + 8512 |
[a__U13(x1)] | = | 4258 |
[U31(x1, x2)] | = | x1 + 4257 |
[a__isNatList#(x1)] | = | x1 + 8512 |
[a__U71(x1)] | = | x1 + 1 |
[U92(x1, x2, x3)] | = | x1 + x2 + 8508 |
[U112(x1, x2, x3)] | = | x2 + 8515 |
[cons(x1, x2)] | = | x1 + x2 + 0 |
[a__U92(x1, x2, x3)] | = | x3 + 8507 |
[a__U61(x1, x2)] | = | 8512 |
[U102(x1, x2, x3)] | = | x1 + 8503 |
[a__U105(x1, x2)] | = | x2 + 8510 |
[a__take(x1, x2)] | = | 4255 |
[U81(x1)] | = | 8512 |
[a__U95#(x1, x2)] | = | x2 + 8512 |
[a__U41#(x1, x2, x3)] | = | x2 + x3 + 8515 |
[tt] | = | 8512 |
[a__U131(x1,...,x4)] | = | x1 + x2 + x4 + 1 |
[a__isNat(x1)] | = | 4255 |
[U13(x1)] | = | 4259 |
[a__U133(x1,...,x4)] | = | x4 + 8515 |
[a__U23(x1)] | = | 8511 |
[a__U96(x1)] | = | 8511 |
[a__isNatKind(x1)] | = | 4270 |
[a__U134#(x1,...,x4)] | = | 56407 |
[U22(x1, x2)] | = | x2 + 4258 |
[U51(x1, x2)] | = | 8512 |
[a__U132#(x1,...,x4)] | = | 56409 |
[a__U103(x1, x2, x3)] | = | x3 + 17015 |
[length(x1)] | = | x1 + 0 |
[a__U112(x1, x2, x3)] | = | x2 + 8514 |
[U41(x1, x2, x3)] | = | x1 + 2 |
[a__U32#(x1, x2)] | = | x2 + 8513 |
[a__zeros] | = | 4255 |
[a__U101(x1, x2, x3)] | = | x2 + x3 + 12771 |
[a__U91#(x1, x2, x3)] | = | x2 + x3 + 8512 |
[U121(x1, x2)] | = | x1 + 12267 |
[a__length(x1)] | = | x1 + 8505 |
[U122(x1)] | = | x1 + 4258 |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__U52(tt) | → | tt | (36) |
a__U62(X) | → | U62(X) | (169) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__U52(X) | → | U52(X) | (167) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__U62(tt) | → | tt | (38) |
a__isNatIListKind(nil) | → | tt | (53) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__U104#(tt,V1,V2) | → | a__U105#(a__isNat(V1),V2) | (363) |
a__U31#(tt,V) | → | a__U32#(a__isNatIListKind(V),V) | (358) |
a__U105#(tt,V2) | → | a__isNatIList#(V2) | (353) |
a__U101#(tt,V1,V2) | → | a__U102#(a__isNatKind(V1),V1,V2) | (350) |
a__U104#(tt,V1,V2) | → | a__isNat#(V1) | (234) |
a__isNatList#(take(V1,V2)) | → | a__U101#(a__isNatKind(V1),V1,V2) | (324) |
a__isNatIList#(V) | → | a__U31#(a__isNatIListKind(V),V) | (227) |
a__U103#(tt,V1,V2) | → | a__U104#(a__isNatIListKind(V2),V1,V2) | (321) |
a__U32#(tt,V) | → | a__isNatList#(V) | (315) |
a__U102#(tt,V1,V2) | → | a__U103#(a__isNatIListKind(V2),V1,V2) | (209) |
a__U44#(tt,V1,V2) | → | a__isNat#(V1) | (195) |
The dependency pairs are split into 2 components.
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (298) |
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (319) |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (360) |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (293) |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (259) |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (223) |
[a__U94#(x1, x2, x3)] | = | x1 + 0 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 55 |
[a__U131#(x1,...,x4)] | = | 56408 |
[U21(x1, x2)] | = | x1 + 54 |
[a__U102(x1, x2, x3)] | = | x1 + x2 + x3 + 4249 |
[a__U45(x1, x2)] | = | x1 + x2 + 4261 |
[isNatList(x1)] | = | 44 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x2 + 54 |
[a__U92#(x1, x2, x3)] | = | 8512 |
[a__U104(x1, x2, x3)] | = | x2 + 27 |
[U136(x1,...,x4)] | = | x4 + 62 |
[a__U112#(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 0 |
[a__U133#(x1,...,x4)] | = | 56408 |
[U105(x1, x2)] | = | x1 + 29 |
[a__U31#(x1, x2)] | = | 8514 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x3 + 1 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | 8512 |
[a__U114(x1, x2)] | = | x1 + x2 + 6 |
[a__isNatIList(x1)] | = | x1 + 27 |
[a__U33(x1)] | = | 58 |
[U106(x1)] | = | 30 |
[a__isNatIListKind#(x1)] | = | 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x2 + 54 |
[U42(x1, x2, x3)] | = | x1 + 59 |
[U91(x1, x2, x3)] | = | x1 + x3 + 51 |
[a__isNat#(x1)] | = | 8512 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | 24635 |
[take(x1, x2)] | = | x1 + x2 + 4258 |
[U71(x1)] | = | 2 |
[a__U62(x1)] | = | 56 |
[a__U44(x1, x2, x3)] | = | x3 + 59 |
[U131(x1,...,x4)] | = | x4 + 2 |
[isNatIList(x1)] | = | 28 |
[U135(x1,...,x4)] | = | x2 + 61 |
[U101(x1, x2, x3)] | = | x2 + 4303 |
[a__U43#(x1, x2, x3)] | = | x3 + 8513 |
[U95(x1, x2)] | = | 55 |
[U111(x1, x2, x3)] | = | 2 |
[U132(x1,...,x4)] | = | x1 + 2 |
[U43(x1, x2, x3)] | = | x2 + 3 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x2 + 28 |
[a__U135#(x1,...,x4)] | = | 24636 |
[a__U44#(x1, x2, x3)] | = | x3 + 8512 |
[U103(x1, x2, x3)] | = | x2 + 4307 |
[a__U111(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U103#(x1, x2, x3)] | = | 8518 |
[U44(x1, x2, x3)] | = | x1 + 60 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | 1 |
[a__U51#(x1, x2)] | = | 0 |
[U23(x1)] | = | x1 + 56 |
[a__U22(x1, x2)] | = | x2 + 54 |
[U93(x1, x2, x3)] | = | 53 |
[a__U94(x1, x2, x3)] | = | x2 + x3 + 53 |
[a__U106(x1)] | = | 29 |
[a__U11#(x1, x2)] | = | 8512 |
[U94(x1, x2, x3)] | = | x3 + 54 |
[zeros] | = | 28 |
[a__U31(x1, x2)] | = | 28 |
[a__U51(x1, x2)] | = | 56 |
[a__U81(x1)] | = | 55 |
[a__take#(x1, x2)] | = | 81043 |
[U12(x1, x2)] | = | x1 + x2 + 55 |
[a__isNatList(x1)] | = | x1 + 43 |
[a__U43(x1, x2, x3)] | = | x1 + x2 + 2 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x2 + 61 |
[a__U42#(x1, x2, x3)] | = | x3 + 8514 |
[a__U41(x1, x2, x3)] | = | x1 + 1 |
[a__U134(x1,...,x4)] | = | x2 + x4 + 59 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | 8512 |
[U104(x1, x2, x3)] | = | 28 |
[a__U122(x1)] | = | 29 |
[a__U21#(x1, x2)] | = | 8512 |
[a__isNatIList#(x1)] | = | x1 + 8510 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[U113(x1, x2, x3)] | = | x2 + 8537 |
[mark#(x1)] | = | 24634 |
[0] | = | 35 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | 1 |
[U134(x1,...,x4)] | = | x1 + 60 |
[a__U21(x1, x2)] | = | 53 |
[a__U32(x1, x2)] | = | x1 + x2 + 1 |
[a__U91(x1, x2, x3)] | = | 50 |
[a__U111#(x1, x2, x3)] | = | 0 |
[nil] | = | 30 |
[isNatIListKind(x1)] | = | 1 |
[U114(x1, x2)] | = | 0 |
[U62(x1)] | = | 1 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | 8519 |
[U45(x1, x2)] | = | 4262 |
[mark(x1)] | = | 26 |
[U133(x1,...,x4)] | = | x2 + x3 + 59 |
[a__U101#(x1, x2, x3)] | = | 8520 |
[a__U11(x1, x2)] | = | 53 |
[U32(x1, x2)] | = | x1 + 17 |
[a__U42(x1, x2, x3)] | = | x2 + 58 |
[a__U93(x1, x2, x3)] | = | x3 + 52 |
[U33(x1)] | = | 59 |
[a__U45#(x1, x2)] | = | x2 + 8511 |
[a__U52(x1)] | = | 56 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x3 + x4 + 60 |
[a__length#(x1)] | = | 1 |
[a__U105#(x1, x2)] | = | 8516 |
[a__U12(x1, x2)] | = | x2 + 54 |
[a__isNatIListKind(x1)] | = | 57 |
[a__U104#(x1, x2, x3)] | = | x1 + 5 |
[isNat(x1)] | = | x1 + 53 |
[U46(x1)] | = | x1 + 28 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | 1 |
[a__U46(x1)] | = | 27 |
[a__U22#(x1, x2)] | = | 8512 |
[a__U113(x1, x2, x3)] | = | x3 + 59 |
[U96(x1)] | = | x1 + 56 |
[a__U13(x1)] | = | 55 |
[U31(x1, x2)] | = | x1 + 29 |
[a__isNatList#(x1)] | = | 8512 |
[a__U71(x1)] | = | x1 + 1 |
[U92(x1, x2, x3)] | = | x1 + x2 + 52 |
[U112(x1, x2, x3)] | = | x2 + 59 |
[cons(x1, x2)] | = | x1 + x2 + 6 |
[a__U92(x1, x2, x3)] | = | x3 + 51 |
[a__U61(x1, x2)] | = | 57 |
[U102(x1, x2, x3)] | = | x1 + 4250 |
[a__U105(x1, x2)] | = | x2 + 28 |
[a__take(x1, x2)] | = | 27 |
[U81(x1)] | = | 56 |
[a__U95#(x1, x2)] | = | 8512 |
[a__U41#(x1, x2, x3)] | = | x3 + 8515 |
[tt] | = | 56 |
[a__U131(x1,...,x4)] | = | x1 + x2 + x4 + 1 |
[a__isNat(x1)] | = | 52 |
[U13(x1)] | = | 56 |
[a__U133(x1,...,x4)] | = | x4 + 58 |
[a__U23(x1)] | = | 55 |
[a__U96(x1)] | = | 55 |
[a__isNatKind(x1)] | = | 54 |
[a__U134#(x1,...,x4)] | = | 56407 |
[U22(x1, x2)] | = | x2 + 55 |
[U51(x1, x2)] | = | 56 |
[a__U132#(x1,...,x4)] | = | 56409 |
[a__U103(x1, x2, x3)] | = | x3 + 4306 |
[length(x1)] | = | x1 + 0 |
[a__U112(x1, x2, x3)] | = | x2 + 58 |
[U41(x1, x2, x3)] | = | x1 + 2 |
[a__U32#(x1, x2)] | = | 8513 |
[a__zeros] | = | 27 |
[a__U101(x1, x2, x3)] | = | x2 + x3 + 4302 |
[a__U91#(x1, x2, x3)] | = | 8512 |
[U121(x1, x2)] | = | x1 + 12267 |
[a__length(x1)] | = | x1 + 37 |
[U122(x1)] | = | x1 + 30 |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__U52(tt) | → | tt | (36) |
a__U62(X) | → | U62(X) | (169) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__U52(X) | → | U52(X) | (167) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__U62(tt) | → | tt | (38) |
a__isNatIListKind(nil) | → | tt | (53) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (298) |
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (319) |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (360) |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (293) |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (259) |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (223) |
The dependency pairs are split into 0 components.
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (340) |
a__U94#(tt,V1,V2) | → | a__isNat#(V1) | (304) |
a__U94#(tt,V1,V2) | → | a__U95#(a__isNat(V1),V2) | (204) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (207) |
a__U95#(tt,V2) | → | a__isNatList#(V2) | (291) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (183) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (253) |
a__U12#(tt,V1) | → | a__isNatList#(V1) | (231) |
a__isNatList#(cons(V1,V2)) | → | a__U91#(a__isNatKind(V1),V1,V2) | (275) |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (192) |
a__U91#(tt,V1,V2) | → | a__U92#(a__isNatKind(V1),V1,V2) | (345) |
a__U92#(tt,V1,V2) | → | a__U93#(a__isNatIListKind(V2),V1,V2) | (269) |
a__U93#(tt,V1,V2) | → | a__U94#(a__isNatIListKind(V2),V1,V2) | (367) |
[a__U94#(x1, x2, x3)] | = | x1 + x2 + x3 + 8457 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | 55 |
[a__U131#(x1,...,x4)] | = | 56408 |
[U21(x1, x2)] | = | x1 + 48 |
[a__U102(x1, x2, x3)] | = | x1 + x2 + x3 + 34 |
[a__U45(x1, x2)] | = | x1 + x2 + 4261 |
[isNatList(x1)] | = | 44 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x2 + 54 |
[a__U92#(x1, x2, x3)] | = | x2 + x3 + 8515 |
[a__U104(x1, x2, x3)] | = | x2 + 27 |
[U136(x1,...,x4)] | = | x4 + 75 |
[a__U112#(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 0 |
[a__U133#(x1,...,x4)] | = | 56408 |
[U105(x1, x2)] | = | x1 + 29 |
[a__U31#(x1, x2)] | = | 8514 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x3 + 2 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | x2 + x3 + 8514 |
[a__U114(x1, x2)] | = | x1 + x2 + 6 |
[a__isNatIList(x1)] | = | x1 + 27 |
[a__U33(x1)] | = | 58 |
[U106(x1)] | = | 30 |
[a__isNatIListKind#(x1)] | = | 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x2 + 54 |
[U42(x1, x2, x3)] | = | x1 + 59 |
[U91(x1, x2, x3)] | = | x1 + x3 + 51 |
[a__isNat#(x1)] | = | x1 + 8512 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | 24635 |
[take(x1, x2)] | = | x1 + x2 + 43 |
[U71(x1)] | = | 2 |
[a__U62(x1)] | = | 56 |
[a__U44(x1, x2, x3)] | = | x3 + 60 |
[U131(x1,...,x4)] | = | x4 + 2 |
[isNatIList(x1)] | = | 28 |
[U135(x1,...,x4)] | = | x2 + 74 |
[U101(x1, x2, x3)] | = | x2 + 88 |
[a__U43#(x1, x2, x3)] | = | 8513 |
[U95(x1, x2)] | = | 55 |
[U111(x1, x2, x3)] | = | 2 |
[U132(x1,...,x4)] | = | x1 + 3 |
[U43(x1, x2, x3)] | = | x2 + 4 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x2 + 28 |
[a__U135#(x1,...,x4)] | = | 24636 |
[a__U44#(x1, x2, x3)] | = | 8512 |
[U103(x1, x2, x3)] | = | x2 + 92 |
[a__U111(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U103#(x1, x2, x3)] | = | 8518 |
[U44(x1, x2, x3)] | = | x1 + 61 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | 1 |
[a__U51#(x1, x2)] | = | 0 |
[U23(x1)] | = | x1 + 50 |
[a__U22(x1, x2)] | = | x2 + 48 |
[U93(x1, x2, x3)] | = | 53 |
[a__U94(x1, x2, x3)] | = | x2 + x3 + 53 |
[a__U106(x1)] | = | 29 |
[a__U11#(x1, x2)] | = | x2 + 8513 |
[U94(x1, x2, x3)] | = | x3 + 54 |
[zeros] | = | 28 |
[a__U31(x1, x2)] | = | 28 |
[a__U51(x1, x2)] | = | 56 |
[a__U81(x1)] | = | 55 |
[a__take#(x1, x2)] | = | 81043 |
[U12(x1, x2)] | = | x1 + x2 + 55 |
[a__isNatList(x1)] | = | x1 + 43 |
[a__U43(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x2 + 74 |
[a__U42#(x1, x2, x3)] | = | 8514 |
[a__U41(x1, x2, x3)] | = | x1 + 1 |
[a__U134(x1,...,x4)] | = | x2 + x4 + 72 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | x2 + 8512 |
[U104(x1, x2, x3)] | = | 28 |
[a__U122(x1)] | = | 29 |
[a__U21#(x1, x2)] | = | x2 + 8512 |
[a__isNatIList#(x1)] | = | 8510 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[U113(x1, x2, x3)] | = | x2 + 8537 |
[mark#(x1)] | = | 24634 |
[0] | = | 31 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | 1 |
[U134(x1,...,x4)] | = | x1 + 73 |
[a__U21(x1, x2)] | = | 47 |
[a__U32(x1, x2)] | = | x1 + x2 + 1 |
[a__U91(x1, x2, x3)] | = | 50 |
[a__U111#(x1, x2, x3)] | = | 0 |
[nil] | = | 30 |
[isNatIListKind(x1)] | = | 1 |
[U114(x1, x2)] | = | 0 |
[U62(x1)] | = | 1 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | 8519 |
[U45(x1, x2)] | = | 4262 |
[mark(x1)] | = | 26 |
[U133(x1,...,x4)] | = | x2 + x3 + 60 |
[a__U101#(x1, x2, x3)] | = | 8520 |
[a__U11(x1, x2)] | = | 53 |
[U32(x1, x2)] | = | x1 + 17 |
[a__U42(x1, x2, x3)] | = | x2 + 58 |
[a__U93(x1, x2, x3)] | = | x3 + 52 |
[U33(x1)] | = | 59 |
[a__U45#(x1, x2)] | = | 8511 |
[a__U52(x1)] | = | 56 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x3 + x4 + 73 |
[a__length#(x1)] | = | 1 |
[a__U105#(x1, x2)] | = | 8516 |
[a__U12(x1, x2)] | = | x2 + 54 |
[a__isNatIListKind(x1)] | = | 56 |
[a__U104#(x1, x2, x3)] | = | x1 + 5 |
[isNat(x1)] | = | x1 + 47 |
[U46(x1)] | = | x1 + 56 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | 1 |
[U61(x1, x2)] | = | 56 |
[a__U46(x1)] | = | 55 |
[a__U22#(x1, x2)] | = | x2 + 8512 |
[a__U113(x1, x2, x3)] | = | x3 + 59 |
[U96(x1)] | = | x1 + 56 |
[a__U13(x1)] | = | 55 |
[U31(x1, x2)] | = | x1 + 29 |
[a__isNatList#(x1)] | = | x1 + 8511 |
[a__U71(x1)] | = | x1 + 1 |
[U92(x1, x2, x3)] | = | x1 + x2 + 52 |
[U112(x1, x2, x3)] | = | x2 + 59 |
[cons(x1, x2)] | = | x1 + x2 + 6 |
[a__U92(x1, x2, x3)] | = | x3 + 51 |
[a__U61(x1, x2)] | = | 56 |
[U102(x1, x2, x3)] | = | x1 + 4250 |
[a__U105(x1, x2)] | = | x2 + 28 |
[a__take(x1, x2)] | = | 27 |
[U81(x1)] | = | 56 |
[a__U95#(x1, x2)] | = | x2 + 8512 |
[a__U41#(x1, x2, x3)] | = | 8515 |
[tt] | = | 56 |
[a__U131(x1,...,x4)] | = | x1 + x2 + x4 + 1 |
[a__isNat(x1)] | = | 46 |
[U13(x1)] | = | 56 |
[a__U133(x1,...,x4)] | = | x4 + 59 |
[a__U23(x1)] | = | 49 |
[a__U96(x1)] | = | 55 |
[a__isNatKind(x1)] | = | 54 |
[a__U134#(x1,...,x4)] | = | 56407 |
[U22(x1, x2)] | = | x2 + 49 |
[U51(x1, x2)] | = | 1 |
[a__U132#(x1,...,x4)] | = | 56409 |
[a__U103(x1, x2, x3)] | = | x3 + 91 |
[length(x1)] | = | x1 + 2 |
[a__U112(x1, x2, x3)] | = | x2 + 58 |
[U41(x1, x2, x3)] | = | x1 + 2 |
[a__U32#(x1, x2)] | = | 8513 |
[a__zeros] | = | 27 |
[a__U101(x1, x2, x3)] | = | x2 + x3 + 87 |
[a__U91#(x1, x2, x3)] | = | x2 + x3 + 8516 |
[U121(x1, x2)] | = | x1 + 12267 |
[a__length(x1)] | = | x1 + 37 |
[U122(x1)] | = | x1 + 30 |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__U52(tt) | → | tt | (36) |
a__U62(X) | → | U62(X) | (169) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__U52(X) | → | U52(X) | (167) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__U62(tt) | → | tt | (38) |
a__isNatIListKind(nil) | → | tt | (53) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (340) |
a__U94#(tt,V1,V2) | → | a__isNat#(V1) | (304) |
a__U94#(tt,V1,V2) | → | a__U95#(a__isNat(V1),V2) | (204) |
a__U95#(tt,V2) | → | a__isNatList#(V2) | (291) |
a__U12#(tt,V1) | → | a__isNatList#(V1) | (231) |
a__isNatList#(cons(V1,V2)) | → | a__U91#(a__isNatKind(V1),V1,V2) | (275) |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (192) |
a__U91#(tt,V1,V2) | → | a__U92#(a__isNatKind(V1),V1,V2) | (345) |
a__U92#(tt,V1,V2) | → | a__U93#(a__isNatIListKind(V2),V1,V2) | (269) |
a__U93#(tt,V1,V2) | → | a__U94#(a__isNatIListKind(V2),V1,V2) | (367) |
The dependency pairs are split into 1 component.
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (207) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (183) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (253) |
[a__U94#(x1, x2, x3)] | = | x1 + 8457 |
[a__isNatKind#(x1)] | = | 0 |
[isNatKind(x1)] | = | x1 + 7 |
[a__U131#(x1,...,x4)] | = | 56408 |
[U21(x1, x2)] | = | x1 + x2 + 6 |
[a__U102(x1, x2, x3)] | = | x1 + x2 + x3 + 187 |
[a__U45(x1, x2)] | = | x1 + x2 + 4261 |
[isNatList(x1)] | = | x1 + 1 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x1 + x2 + 6 |
[a__U92#(x1, x2, x3)] | = | 8515 |
[a__U104(x1, x2, x3)] | = | x2 + 0 |
[U136(x1,...,x4)] | = | x3 + x4 + 4 |
[a__U112#(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 3 |
[a__U133#(x1,...,x4)] | = | 56408 |
[U105(x1, x2)] | = | x1 + x2 + 2 |
[a__U31#(x1, x2)] | = | 8514 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x3 + 0 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | 8514 |
[a__U114(x1, x2)] | = | x1 + x2 + 53853 |
[a__isNatIList(x1)] | = | x1 + 4 |
[a__U33(x1)] | = | 58 |
[U106(x1)] | = | 8 |
[a__isNatIListKind#(x1)] | = | 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x2 + 6 |
[U42(x1, x2, x3)] | = | x1 + x2 + 10 |
[U91(x1, x2, x3)] | = | x1 + x3 + 21 |
[a__isNat#(x1)] | = | x1 + 8510 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | 24635 |
[take(x1, x2)] | = | x1 + x2 + 24 |
[U71(x1)] | = | 17985 |
[a__U62(x1)] | = | 8 |
[a__U44(x1, x2, x3)] | = | x3 + 9 |
[U131(x1,...,x4)] | = | x2 + 26 |
[isNatIList(x1)] | = | 1 |
[U135(x1,...,x4)] | = | x2 + x4 + 12 |
[U101(x1, x2, x3)] | = | x2 + x3 + 193 |
[a__U43#(x1, x2, x3)] | = | 8513 |
[U95(x1, x2)] | = | x1 + 7 |
[U111(x1, x2, x3)] | = | x3 + 53840 |
[U132(x1,...,x4)] | = | x1 + x2 + 63 |
[U43(x1, x2, x3)] | = | x2 + 20424 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x2 + 93 |
[a__U135#(x1,...,x4)] | = | 24636 |
[a__U44#(x1, x2, x3)] | = | 8512 |
[U103(x1, x2, x3)] | = | x2 + 201 |
[a__U111(x1, x2, x3)] | = | x1 + x2 + x3 + 53841 |
[a__U103#(x1, x2, x3)] | = | 8518 |
[U44(x1, x2, x3)] | = | x1 + x3 + 6 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | 1 |
[a__U51#(x1, x2)] | = | 0 |
[U23(x1)] | = | x1 + 8 |
[a__U22(x1, x2)] | = | x2 + 6 |
[U93(x1, x2, x3)] | = | 10258 |
[a__U94(x1, x2, x3)] | = | x2 + x3 + 5 |
[a__U106(x1)] | = | 7 |
[a__U11#(x1, x2)] | = | 8513 |
[U94(x1, x2, x3)] | = | x1 + x3 + 1 |
[zeros] | = | 3 |
[a__U31(x1, x2)] | = | 5 |
[a__U51(x1, x2)] | = | 8 |
[a__U81(x1)] | = | 7 |
[a__take#(x1, x2)] | = | 81043 |
[U12(x1, x2)] | = | x1 + x2 + 51 |
[a__isNatList(x1)] | = | x1 + 18 |
[a__U43(x1, x2, x3)] | = | x1 + x2 + 0 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x2 + 12 |
[a__U42#(x1, x2, x3)] | = | 8514 |
[a__U41(x1, x2, x3)] | = | x1 + x2 + 0 |
[a__U134(x1,...,x4)] | = | x2 + x4 + 10 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | 8512 |
[U104(x1, x2, x3)] | = | x2 + 22549 |
[a__U122(x1)] | = | 94 |
[a__U21#(x1, x2)] | = | x2 + 8512 |
[a__isNatIList#(x1)] | = | 8510 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | 0 |
[U113(x1, x2, x3)] | = | x2 + 28216 |
[mark#(x1)] | = | 24634 |
[0] | = | 4 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | 1 |
[U134(x1,...,x4)] | = | x1 + x4 + 11 |
[a__U21(x1, x2)] | = | 5 |
[a__U32(x1, x2)] | = | x1 + x2 + 0 |
[a__U91(x1, x2, x3)] | = | 20 |
[a__U111#(x1, x2, x3)] | = | 0 |
[nil] | = | 95 |
[isNatIListKind(x1)] | = | 10 |
[U114(x1, x2)] | = | 10780 |
[U62(x1)] | = | 5 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | 8519 |
[U45(x1, x2)] | = | 4262 |
[mark(x1)] | = | x1 + 2 |
[U133(x1,...,x4)] | = | x2 + x3 + x4 + 10 |
[a__U101#(x1, x2, x3)] | = | 8520 |
[a__U11(x1, x2)] | = | 5 |
[U32(x1, x2)] | = | 24132 |
[a__U42(x1, x2, x3)] | = | x2 + 9 |
[a__U93(x1, x2, x3)] | = | x1 + x3 + 0 |
[U33(x1)] | = | 59 |
[a__U45#(x1, x2)] | = | 8511 |
[a__U52(x1)] | = | 8 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x3 + x4 + 11 |
[a__length#(x1)] | = | 1 |
[a__U105#(x1, x2)] | = | 8516 |
[a__U12(x1, x2)] | = | x2 + 6 |
[a__isNatIListKind(x1)] | = | 34 |
[a__U104#(x1, x2, x3)] | = | x1 + 5 |
[isNat(x1)] | = | x1 + 2 |
[U46(x1)] | = | x1 + 9259 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | 4 |
[U61(x1, x2)] | = | 8 |
[a__U46(x1)] | = | 0 |
[a__U22#(x1, x2)] | = | x2 + 8511 |
[a__U113(x1, x2, x3)] | = | x1 + x3 + 53850 |
[U96(x1)] | = | x1 + 8 |
[a__U13(x1)] | = | 7 |
[U31(x1, x2)] | = | x1 + 6 |
[a__isNatList#(x1)] | = | 8511 |
[a__U71(x1)] | = | x1 + 0 |
[U92(x1, x2, x3)] | = | x2 + 16 |
[U112(x1, x2, x3)] | = | x2 + 53851 |
[cons(x1, x2)] | = | x1 + x2 + 1 |
[a__U92(x1, x2, x3)] | = | x1 + x3 + 15 |
[a__U61(x1, x2)] | = | 34 |
[U102(x1, x2, x3)] | = | x1 + 188 |
[a__U105(x1, x2)] | = | x2 + 1 |
[a__take(x1, x2)] | = | x1 + 25 |
[U81(x1)] | = | 8 |
[a__U95#(x1, x2)] | = | 8512 |
[a__U41#(x1, x2, x3)] | = | 8515 |
[tt] | = | 8 |
[a__U131(x1,...,x4)] | = | x1 + x2 + x4 + 25 |
[a__isNat(x1)] | = | x1 + 1 |
[U13(x1)] | = | 52 |
[a__U133(x1,...,x4)] | = | x4 + 9 |
[a__U23(x1)] | = | 7 |
[a__U96(x1)] | = | 7 |
[a__isNatKind(x1)] | = | 6 |
[a__U134#(x1,...,x4)] | = | 56407 |
[U22(x1, x2)] | = | x2 + 7 |
[U51(x1, x2)] | = | 2 |
[a__U132#(x1,...,x4)] | = | 56409 |
[a__U103(x1, x2, x3)] | = | x3 + 196 |
[length(x1)] | = | x1 + 3 |
[a__U112(x1, x2, x3)] | = | x2 + 53850 |
[U41(x1, x2, x3)] | = | x2 + 26863 |
[a__U32#(x1, x2)] | = | 8513 |
[a__zeros] | = | 7 |
[a__U101(x1, x2, x3)] | = | x2 + x3 + 192 |
[a__U91#(x1, x2, x3)] | = | 8516 |
[U121(x1, x2)] | = | x1 + 94 |
[a__length(x1)] | = | x1 + 53857 |
[U122(x1)] | = | x1 + 20 |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__U52(tt) | → | tt | (36) |
a__U62(X) | → | U62(X) | (169) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__U52(X) | → | U52(X) | (167) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__U62(tt) | → | tt | (38) |
a__isNatIListKind(nil) | → | tt | (53) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (207) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (183) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (253) |
The dependency pairs are split into 0 components.
a__isNatIListKind#(take(V1,V2)) | → | a__isNatKind#(V1) | (270) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (264) |
a__U61#(tt,V2) | → | a__isNatIListKind#(V2) | (248) |
a__isNatIListKind#(take(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (336) |
a__U51#(tt,V2) | → | a__isNatIListKind#(V2) | (238) |
a__isNatIListKind#(cons(V1,V2)) | → | a__isNatKind#(V1) | (323) |
a__isNatIListKind#(cons(V1,V2)) | → | a__U51#(a__isNatKind(V1),V2) | (226) |
a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | (186) |
[a__U94#(x1, x2, x3)] | = | x1 + 8457 |
[a__isNatKind#(x1)] | = | x1 + 0 |
[isNatKind(x1)] | = | x1 + 9 |
[a__U131#(x1,...,x4)] | = | 56408 |
[U21(x1, x2)] | = | x1 + x2 + 10 |
[a__U102(x1, x2, x3)] | = | x1 + x2 + x3 + 40 |
[a__U45(x1, x2)] | = | x1 + x2 + 4261 |
[isNatList(x1)] | = | x1 + 22 |
[a__U71#(x1)] | = | 0 |
[U11(x1, x2)] | = | x1 + x2 + 4 |
[a__U92#(x1, x2, x3)] | = | 8515 |
[a__U104(x1, x2, x3)] | = | x2 + 0 |
[U136(x1,...,x4)] | = | x3 + x4 + 1 |
[a__U112#(x1, x2, x3)] | = | 2 |
[s(x1)] | = | x1 + 2 |
[a__U133#(x1,...,x4)] | = | 56408 |
[U105(x1, x2)] | = | x1 + x2 + 2 |
[a__U31#(x1, x2)] | = | 8514 |
[a__U132(x1,...,x4)] | = | x1 + x2 + x3 + 0 |
[a__U33#(x1)] | = | 0 |
[a__U93#(x1, x2, x3)] | = | 8514 |
[a__U114(x1, x2)] | = | x1 + x2 + 27055 |
[a__isNatIList(x1)] | = | x1 + 8 |
[a__U33(x1)] | = | 58 |
[U106(x1)] | = | 3 |
[a__isNatIListKind#(x1)] | = | x1 + 0 |
[a__U23#(x1)] | = | 0 |
[a__U95(x1, x2)] | = | x2 + 5 |
[U42(x1, x2, x3)] | = | x1 + x2 + 16 |
[U91(x1, x2, x3)] | = | x1 + x3 + 30 |
[a__isNat#(x1)] | = | 8510 |
[a__U106#(x1)] | = | 0 |
[a__U136#(x1,...,x4)] | = | 24635 |
[take(x1, x2)] | = | x1 + x2 + 21 |
[U71(x1)] | = | 6710 |
[a__U62(x1)] | = | 10 |
[a__U44(x1, x2, x3)] | = | x3 + 472 |
[U131(x1,...,x4)] | = | x2 + 18 |
[isNatIList(x1)] | = | 3 |
[U135(x1,...,x4)] | = | x2 + x4 + 15 |
[U101(x1, x2, x3)] | = | x2 + x3 + 48 |
[a__U43#(x1, x2, x3)] | = | 8513 |
[U95(x1, x2)] | = | x1 + 28720 |
[U111(x1, x2, x3)] | = | x3 + 27040 |
[U132(x1,...,x4)] | = | x1 + x2 + 63 |
[U43(x1, x2, x3)] | = | x2 + 20424 |
[a__U13#(x1)] | = | 0 |
[a__U121(x1, x2)] | = | x2 + 25 |
[a__U135#(x1,...,x4)] | = | 24636 |
[a__U44#(x1, x2, x3)] | = | 8512 |
[U103(x1, x2, x3)] | = | x2 + 52 |
[a__U111(x1, x2, x3)] | = | x1 + x2 + x3 + 27041 |
[a__U103#(x1, x2, x3)] | = | 8518 |
[U44(x1, x2, x3)] | = | x1 + x3 + 469 |
[a__U46#(x1)] | = | 0 |
[a__U114#(x1, x2)] | = | 1 |
[a__U51#(x1, x2)] | = | x2 + 2 |
[U23(x1)] | = | x1 + 9721 |
[a__U22(x1, x2)] | = | x2 + 8 |
[U93(x1, x2, x3)] | = | 10258 |
[a__U94(x1, x2, x3)] | = | x2 + x3 + 4 |
[a__U106(x1)] | = | 2 |
[a__U11#(x1, x2)] | = | 8513 |
[U94(x1, x2, x3)] | = | x1 + x3 + 1 |
[zeros] | = | 1 |
[a__U31(x1, x2)] | = | 9 |
[a__U51(x1, x2)] | = | 10 |
[a__U81(x1)] | = | 9 |
[a__take#(x1, x2)] | = | 81043 |
[U12(x1, x2)] | = | x1 + x2 + 49 |
[a__isNatList(x1)] | = | x1 + 25 |
[a__U43(x1, x2, x3)] | = | x1 + x2 + 0 |
[a__U62#(x1)] | = | 0 |
[a__U136(x1,...,x4)] | = | x2 + 25 |
[a__U42#(x1, x2, x3)] | = | 8514 |
[a__U41(x1, x2, x3)] | = | x1 + x2 + 4 |
[a__U134(x1,...,x4)] | = | x2 + x4 + 14 |
[a__U122#(x1)] | = | 0 |
[a__U12#(x1, x2)] | = | 8512 |
[U104(x1, x2, x3)] | = | x2 + 27772 |
[a__U122(x1)] | = | 94 |
[a__U21#(x1, x2)] | = | 8512 |
[a__isNatIList#(x1)] | = | 8510 |
[a__U81#(x1)] | = | 0 |
[a__U61#(x1, x2)] | = | x2 + 1 |
[U113(x1, x2, x3)] | = | x2 + 7109 |
[mark#(x1)] | = | 24634 |
[0] | = | 2 |
[a__zeros#] | = | 0 |
[a__U113#(x1, x2, x3)] | = | 1 |
[U134(x1,...,x4)] | = | x1 + x4 + 15 |
[a__U21(x1, x2)] | = | 7 |
[a__U32(x1, x2)] | = | x1 + x2 + 0 |
[a__U91(x1, x2, x3)] | = | 29 |
[a__U111#(x1, x2, x3)] | = | 0 |
[nil] | = | 95 |
[isNatIListKind(x1)] | = | 10 |
[U114(x1, x2)] | = | 3044 |
[U62(x1)] | = | 5 |
[a__U52#(x1)] | = | 0 |
[a__U102#(x1, x2, x3)] | = | 8519 |
[U45(x1, x2)] | = | 4262 |
[mark(x1)] | = | x1 + 2 |
[U133(x1,...,x4)] | = | x2 + x3 + x4 + 12 |
[a__U101#(x1, x2, x3)] | = | 8520 |
[a__U11(x1, x2)] | = | 3 |
[U32(x1, x2)] | = | 24132 |
[a__U42(x1, x2, x3)] | = | x2 + 15 |
[a__U93(x1, x2, x3)] | = | x1 + x3 + 0 |
[U33(x1)] | = | 59 |
[a__U45#(x1, x2)] | = | 8511 |
[a__U52(x1)] | = | 10 |
[a__U96#(x1)] | = | 0 |
[a__U135(x1,...,x4)] | = | x1 + x3 + x4 + 14 |
[a__length#(x1)] | = | 1 |
[a__U105#(x1, x2)] | = | 8516 |
[a__U12(x1, x2)] | = | x2 + 4 |
[a__isNatIListKind(x1)] | = | 34 |
[a__U104#(x1, x2, x3)] | = | x1 + 5 |
[isNat(x1)] | = | x1 + 22560 |
[U46(x1)] | = | x1 + 1 |
[a__U121#(x1, x2)] | = | 0 |
[U52(x1)] | = | 5 |
[U61(x1, x2)] | = | 1 |
[a__U46(x1)] | = | 0 |
[a__U22#(x1, x2)] | = | 8511 |
[a__U113(x1, x2, x3)] | = | x1 + x3 + 27052 |
[U96(x1)] | = | x1 + 31698 |
[a__U13(x1)] | = | 5 |
[U31(x1, x2)] | = | x1 + 10 |
[a__isNatList#(x1)] | = | 8511 |
[a__U71(x1)] | = | x1 + 0 |
[U92(x1, x2, x3)] | = | x2 + 23 |
[U112(x1, x2, x3)] | = | x2 + 27053 |
[cons(x1, x2)] | = | x1 + x2 + 3 |
[a__U92(x1, x2, x3)] | = | x1 + x3 + 22 |
[a__U61(x1, x2)] | = | 34 |
[U102(x1, x2, x3)] | = | x1 + 41 |
[a__U105(x1, x2)] | = | x2 + 1 |
[a__take(x1, x2)] | = | x1 + 22 |
[U81(x1)] | = | 20449 |
[a__U95#(x1, x2)] | = | 8512 |
[a__U41#(x1, x2, x3)] | = | 8515 |
[tt] | = | 10 |
[a__U131(x1,...,x4)] | = | x1 + x2 + x4 + 17 |
[a__isNat(x1)] | = | x1 + 1 |
[U13(x1)] | = | 50 |
[a__U133(x1,...,x4)] | = | x4 + 11 |
[a__U23(x1)] | = | 9 |
[a__U96(x1)] | = | 6 |
[a__isNatKind(x1)] | = | 8 |
[a__U134#(x1,...,x4)] | = | 56407 |
[U22(x1, x2)] | = | x2 + 9 |
[U51(x1, x2)] | = | 2 |
[a__U132#(x1,...,x4)] | = | 56409 |
[a__U103(x1, x2, x3)] | = | x3 + 51 |
[length(x1)] | = | x1 + 1 |
[a__U112(x1, x2, x3)] | = | x2 + 27052 |
[U41(x1, x2, x3)] | = | x2 + 26867 |
[a__U32#(x1, x2)] | = | 8513 |
[a__zeros] | = | 4 |
[a__U101(x1, x2, x3)] | = | x2 + x3 + 47 |
[a__U91#(x1, x2, x3)] | = | 8516 |
[U121(x1, x2)] | = | x1 + 26 |
[a__length(x1)] | = | x1 + 27062 |
[U122(x1)] | = | x1 + 20 |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__U52(tt) | → | tt | (36) |
a__U62(X) | → | U62(X) | (169) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__U52(X) | → | U52(X) | (167) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__U62(tt) | → | tt | (38) |
a__isNatIListKind(nil) | → | tt | (53) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__isNatIListKind#(take(V1,V2)) | → | a__isNatKind#(V1) | (270) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (264) |
a__U61#(tt,V2) | → | a__isNatIListKind#(V2) | (248) |
a__isNatIListKind#(take(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (336) |
a__U51#(tt,V2) | → | a__isNatIListKind#(V2) | (238) |
a__isNatIListKind#(cons(V1,V2)) | → | a__isNatKind#(V1) | (323) |
a__isNatIListKind#(cons(V1,V2)) | → | a__U51#(a__isNatKind(V1),V2) | (226) |
a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | (186) |
The dependency pairs are split into 0 components.