The rewrite relation of the following TRS is considered.
There are 177 ruless (increase limit for explicit display).
The evaluation strategy is innermost.There are 196 ruless (increase limit for explicit display).
The dependency pairs are split into 3 components.
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (273) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (275) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (278) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (281) |
mark#(U105(X1,X2)) | → | mark#(X1) | (283) |
mark#(U106(X)) | → | mark#(X) | (286) |
mark#(U11(X1,X2)) | → | mark#(X1) | (289) |
mark#(U12(X1,X2)) | → | mark#(X1) | (291) |
mark#(U111(X1,X2,X3)) | → | a__U111#(mark(X1),X2,X3) | (292) |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (190) |
a__U112#(tt,L,N) | → | a__U113#(a__isNat(N),L,N) | (192) |
a__U113#(tt,L,N) | → | a__U114#(a__isNatKind(N),L) | (194) |
a__U114#(tt,L) | → | a__length#(mark(L)) | (196) |
a__length#(cons(N,L)) | → | a__U111#(a__isNatList(L),L,N) | (265) |
a__U114#(tt,L) | → | mark#(L) | (197) |
mark#(U111(X1,X2,X3)) | → | mark#(X1) | (293) |
mark#(U112(X1,X2,X3)) | → | a__U112#(mark(X1),X2,X3) | (294) |
mark#(U112(X1,X2,X3)) | → | mark#(X1) | (295) |
mark#(U113(X1,X2,X3)) | → | a__U113#(mark(X1),X2,X3) | (296) |
mark#(U113(X1,X2,X3)) | → | mark#(X1) | (297) |
mark#(U114(X1,X2)) | → | a__U114#(mark(X1),X2) | (298) |
mark#(U114(X1,X2)) | → | mark#(X1) | (299) |
mark#(length(X)) | → | a__length#(mark(X)) | (300) |
mark#(length(X)) | → | mark#(X) | (301) |
mark#(U13(X)) | → | mark#(X) | (303) |
mark#(U121(X1,X2)) | → | mark#(X1) | (306) |
mark#(U122(X)) | → | mark#(X) | (308) |
mark#(U131(X1,X2,X3,X4)) | → | a__U131#(mark(X1),X2,X3,X4) | (309) |
a__U131#(tt,IL,M,N) | → | a__U132#(a__isNatIListKind(IL),IL,M,N) | (202) |
a__U132#(tt,IL,M,N) | → | a__U133#(a__isNat(M),IL,M,N) | (204) |
a__U133#(tt,IL,M,N) | → | a__U134#(a__isNatKind(M),IL,M,N) | (206) |
a__U134#(tt,IL,M,N) | → | a__U135#(a__isNat(N),IL,M,N) | (208) |
a__U135#(tt,IL,M,N) | → | a__U136#(a__isNatKind(N),IL,M,N) | (210) |
a__U136#(tt,IL,M,N) | → | mark#(N) | (212) |
mark#(U131(X1,X2,X3,X4)) | → | mark#(X1) | (310) |
mark#(U132(X1,X2,X3,X4)) | → | a__U132#(mark(X1),X2,X3,X4) | (311) |
mark#(U132(X1,X2,X3,X4)) | → | mark#(X1) | (312) |
mark#(U133(X1,X2,X3,X4)) | → | a__U133#(mark(X1),X2,X3,X4) | (313) |
mark#(U133(X1,X2,X3,X4)) | → | mark#(X1) | (314) |
mark#(U134(X1,X2,X3,X4)) | → | a__U134#(mark(X1),X2,X3,X4) | (315) |
mark#(U134(X1,X2,X3,X4)) | → | mark#(X1) | (316) |
mark#(U135(X1,X2,X3,X4)) | → | a__U135#(mark(X1),X2,X3,X4) | (317) |
mark#(U135(X1,X2,X3,X4)) | → | mark#(X1) | (318) |
mark#(U136(X1,X2,X3,X4)) | → | a__U136#(mark(X1),X2,X3,X4) | (319) |
mark#(U136(X1,X2,X3,X4)) | → | mark#(X1) | (320) |
mark#(take(X1,X2)) | → | a__take#(mark(X1),mark(X2)) | (321) |
a__take#(s(M),cons(N,IL)) | → | a__U131#(a__isNatIList(IL),IL,M,N) | (269) |
mark#(take(X1,X2)) | → | mark#(X1) | (322) |
mark#(take(X1,X2)) | → | mark#(X2) | (323) |
mark#(U21(X1,X2)) | → | mark#(X1) | (325) |
mark#(U22(X1,X2)) | → | mark#(X1) | (327) |
mark#(U23(X)) | → | mark#(X) | (329) |
mark#(U31(X1,X2)) | → | mark#(X1) | (331) |
mark#(U32(X1,X2)) | → | mark#(X1) | (333) |
mark#(U33(X)) | → | mark#(X) | (335) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (337) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (339) |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (341) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (343) |
mark#(U45(X1,X2)) | → | mark#(X1) | (345) |
mark#(U46(X)) | → | mark#(X) | (347) |
mark#(U51(X1,X2)) | → | mark#(X1) | (349) |
mark#(U52(X)) | → | mark#(X) | (351) |
mark#(U61(X1,X2)) | → | mark#(X1) | (353) |
mark#(U62(X)) | → | mark#(X) | (355) |
mark#(U71(X)) | → | mark#(X) | (357) |
mark#(U81(X)) | → | mark#(X) | (359) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (361) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (363) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (365) |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (367) |
mark#(U95(X1,X2)) | → | mark#(X1) | (369) |
mark#(U96(X)) | → | mark#(X) | (371) |
mark#(cons(X1,X2)) | → | mark#(X1) | (372) |
mark#(s(X)) | → | mark#(X) | (373) |
[a__length#(x1)] | = | x1 |
[a__take#(x1, x2)] | = | 1 + x2 |
[a__U111#(x1, x2, x3)] | = | x2 + x3 |
[a__U112#(x1, x2, x3)] | = | x2 |
[a__U113#(x1, x2, x3)] | = | x2 |
[a__U114#(x1, x2)] | = | x2 |
[a__U131#(x1,...,x4)] | = | 1 + x2 + 2 · x4 |
[a__U132#(x1,...,x4)] | = | 1 + x2 + 2 · x4 |
[a__U133#(x1,...,x4)] | = | 1 + 2 · x4 |
[a__U134#(x1,...,x4)] | = | x4 |
[a__U135#(x1,...,x4)] | = | x4 |
[a__U136#(x1,...,x4)] | = | x4 |
[mark(x1)] | = | x1 |
[zeros] | = | 0 |
[a__zeros] | = | 0 |
[U101(x1, x2, x3)] | = | 2 · x1 |
[a__U101(x1, x2, x3)] | = | 2 · x1 |
[U102(x1, x2, x3)] | = | x1 |
[a__U102(x1, x2, x3)] | = | x1 |
[isNatKind(x1)] | = | 0 |
[a__isNatKind(x1)] | = | 0 |
[U103(x1, x2, x3)] | = | x1 |
[a__U103(x1, x2, x3)] | = | x1 |
[isNatIListKind(x1)] | = | 0 |
[a__isNatIListKind(x1)] | = | 0 |
[U104(x1, x2, x3)] | = | 2 · x1 |
[a__U104(x1, x2, x3)] | = | 2 · x1 |
[U105(x1, x2)] | = | x1 |
[a__U105(x1, x2)] | = | x1 |
[isNat(x1)] | = | 0 |
[a__isNat(x1)] | = | 0 |
[U106(x1)] | = | x1 |
[a__U106(x1)] | = | x1 |
[isNatIList(x1)] | = | 0 |
[a__isNatIList(x1)] | = | 0 |
[U11(x1, x2)] | = | 2 · x1 |
[a__U11(x1, x2)] | = | 2 · x1 |
[U12(x1, x2)] | = | 2 · x1 |
[a__U12(x1, x2)] | = | 2 · x1 |
[U111(x1, x2, x3)] | = | 2 · x1 + x2 + x3 |
[a__U111(x1, x2, x3)] | = | 2 · x1 + x2 + x3 |
[U112(x1, x2, x3)] | = | 2 · x1 + x2 |
[a__U112(x1, x2, x3)] | = | 2 · x1 + x2 |
[U113(x1, x2, x3)] | = | x1 + x2 |
[a__U113(x1, x2, x3)] | = | x1 + x2 |
[U114(x1, x2)] | = | x1 + x2 |
[a__U114(x1, x2)] | = | x1 + x2 |
[length(x1)] | = | x1 |
[a__length(x1)] | = | x1 |
[U13(x1)] | = | x1 |
[a__U13(x1)] | = | x1 |
[isNatList(x1)] | = | 0 |
[a__isNatList(x1)] | = | 0 |
[U121(x1, x2)] | = | 1 + x1 |
[a__U121(x1, x2)] | = | 1 + x1 |
[U122(x1)] | = | 1 + 2 · x1 |
[a__U122(x1)] | = | 1 + 2 · x1 |
[U131(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[a__U131(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[U132(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[a__U132(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[U133(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[a__U133(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[U134(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[a__U134(x1,...,x4)] | = | 1 + 2 · x1 + x2 + x3 + 2 · x4 |
[U135(x1,...,x4)] | = | 1 + x1 + x2 + x3 + 2 · x4 |
[a__U135(x1,...,x4)] | = | 1 + x1 + x2 + x3 + 2 · x4 |
[U136(x1,...,x4)] | = | 1 + x1 + x2 + x3 + 2 · x4 |
[a__U136(x1,...,x4)] | = | 1 + x1 + x2 + x3 + 2 · x4 |
[take(x1, x2)] | = | 1 + x1 + x2 |
[a__take(x1, x2)] | = | 1 + x1 + x2 |
[U21(x1, x2)] | = | x1 |
[a__U21(x1, x2)] | = | x1 |
[U22(x1, x2)] | = | 2 · x1 |
[a__U22(x1, x2)] | = | 2 · x1 |
[U23(x1)] | = | x1 |
[a__U23(x1)] | = | x1 |
[U31(x1, x2)] | = | x1 |
[a__U31(x1, x2)] | = | x1 |
[U32(x1, x2)] | = | x1 |
[a__U32(x1, x2)] | = | x1 |
[U33(x1)] | = | x1 |
[a__U33(x1)] | = | x1 |
[U41(x1, x2, x3)] | = | 2 · x1 |
[a__U41(x1, x2, x3)] | = | 2 · x1 |
[U42(x1, x2, x3)] | = | x1 |
[a__U42(x1, x2, x3)] | = | x1 |
[U43(x1, x2, x3)] | = | x1 |
[a__U43(x1, x2, x3)] | = | x1 |
[U44(x1, x2, x3)] | = | x1 |
[a__U44(x1, x2, x3)] | = | x1 |
[U45(x1, x2)] | = | 2 · x1 |
[a__U45(x1, x2)] | = | 2 · x1 |
[U46(x1)] | = | 2 · x1 |
[a__U46(x1)] | = | 2 · x1 |
[U51(x1, x2)] | = | x1 |
[a__U51(x1, x2)] | = | x1 |
[U52(x1)] | = | 2 · x1 |
[a__U52(x1)] | = | 2 · x1 |
[U61(x1, x2)] | = | x1 |
[a__U61(x1, x2)] | = | x1 |
[U62(x1)] | = | x1 |
[a__U62(x1)] | = | x1 |
[U71(x1)] | = | 2 · x1 |
[a__U71(x1)] | = | 2 · x1 |
[U81(x1)] | = | 2 · x1 |
[a__U81(x1)] | = | 2 · x1 |
[U91(x1, x2, x3)] | = | x1 |
[a__U91(x1, x2, x3)] | = | x1 |
[U92(x1, x2, x3)] | = | x1 |
[a__U92(x1, x2, x3)] | = | x1 |
[U93(x1, x2, x3)] | = | 2 · x1 |
[a__U93(x1, x2, x3)] | = | 2 · x1 |
[U94(x1, x2, x3)] | = | 2 · x1 |
[a__U94(x1, x2, x3)] | = | 2 · x1 |
[U95(x1, x2)] | = | 2 · x1 |
[a__U95(x1, x2)] | = | 2 · x1 |
[U96(x1)] | = | x1 |
[a__U96(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x1 + x2 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[nil] | = | 0 |
[mark#(x1)] | = | x1 |
mark#(U121(X1,X2)) | → | mark#(X1) | (306) |
mark#(U122(X)) | → | mark#(X) | (308) |
a__U133#(tt,IL,M,N) | → | a__U134#(a__isNatKind(M),IL,M,N) | (206) |
mark#(U131(X1,X2,X3,X4)) | → | mark#(X1) | (310) |
mark#(U132(X1,X2,X3,X4)) | → | mark#(X1) | (312) |
mark#(U133(X1,X2,X3,X4)) | → | mark#(X1) | (314) |
mark#(U134(X1,X2,X3,X4)) | → | a__U134#(mark(X1),X2,X3,X4) | (315) |
mark#(U134(X1,X2,X3,X4)) | → | mark#(X1) | (316) |
mark#(U135(X1,X2,X3,X4)) | → | a__U135#(mark(X1),X2,X3,X4) | (317) |
mark#(U135(X1,X2,X3,X4)) | → | mark#(X1) | (318) |
mark#(U136(X1,X2,X3,X4)) | → | a__U136#(mark(X1),X2,X3,X4) | (319) |
mark#(U136(X1,X2,X3,X4)) | → | mark#(X1) | (320) |
mark#(take(X1,X2)) | → | mark#(X1) | (322) |
mark#(take(X1,X2)) | → | mark#(X2) | (323) |
The dependency pairs are split into 1 component.
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (275) |
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (273) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (278) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (281) |
mark#(U105(X1,X2)) | → | mark#(X1) | (283) |
mark#(U106(X)) | → | mark#(X) | (286) |
mark#(U11(X1,X2)) | → | mark#(X1) | (289) |
mark#(U12(X1,X2)) | → | mark#(X1) | (291) |
mark#(U111(X1,X2,X3)) | → | a__U111#(mark(X1),X2,X3) | (292) |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (190) |
a__U112#(tt,L,N) | → | a__U113#(a__isNat(N),L,N) | (192) |
a__U113#(tt,L,N) | → | a__U114#(a__isNatKind(N),L) | (194) |
a__U114#(tt,L) | → | a__length#(mark(L)) | (196) |
a__length#(cons(N,L)) | → | a__U111#(a__isNatList(L),L,N) | (265) |
a__U114#(tt,L) | → | mark#(L) | (197) |
mark#(U111(X1,X2,X3)) | → | mark#(X1) | (293) |
mark#(U112(X1,X2,X3)) | → | a__U112#(mark(X1),X2,X3) | (294) |
mark#(U112(X1,X2,X3)) | → | mark#(X1) | (295) |
mark#(U113(X1,X2,X3)) | → | a__U113#(mark(X1),X2,X3) | (296) |
mark#(U113(X1,X2,X3)) | → | mark#(X1) | (297) |
mark#(U114(X1,X2)) | → | a__U114#(mark(X1),X2) | (298) |
mark#(U114(X1,X2)) | → | mark#(X1) | (299) |
mark#(length(X)) | → | a__length#(mark(X)) | (300) |
mark#(length(X)) | → | mark#(X) | (301) |
mark#(U13(X)) | → | mark#(X) | (303) |
mark#(U21(X1,X2)) | → | mark#(X1) | (325) |
mark#(U22(X1,X2)) | → | mark#(X1) | (327) |
mark#(U23(X)) | → | mark#(X) | (329) |
mark#(U31(X1,X2)) | → | mark#(X1) | (331) |
mark#(U32(X1,X2)) | → | mark#(X1) | (333) |
mark#(U33(X)) | → | mark#(X) | (335) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (337) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (339) |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (341) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (343) |
mark#(U45(X1,X2)) | → | mark#(X1) | (345) |
mark#(U46(X)) | → | mark#(X) | (347) |
mark#(U51(X1,X2)) | → | mark#(X1) | (349) |
mark#(U52(X)) | → | mark#(X) | (351) |
mark#(U61(X1,X2)) | → | mark#(X1) | (353) |
mark#(U62(X)) | → | mark#(X) | (355) |
mark#(U71(X)) | → | mark#(X) | (357) |
mark#(U81(X)) | → | mark#(X) | (359) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (361) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (363) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (365) |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (367) |
mark#(U95(X1,X2)) | → | mark#(X1) | (369) |
mark#(U96(X)) | → | mark#(X) | (371) |
mark#(cons(X1,X2)) | → | mark#(X1) | (372) |
mark#(s(X)) | → | mark#(X) | (373) |
[a__length#(x1)] | = | x1 |
[a__U111#(x1, x2, x3)] | = | x2 + 2 · x3 |
[a__U112#(x1, x2, x3)] | = | x2 |
[a__U113#(x1, x2, x3)] | = | x2 |
[a__U114#(x1, x2)] | = | x2 |
[mark(x1)] | = | x1 |
[zeros] | = | 0 |
[a__zeros] | = | 0 |
[U101(x1, x2, x3)] | = | x1 |
[a__U101(x1, x2, x3)] | = | x1 |
[U102(x1, x2, x3)] | = | x1 |
[a__U102(x1, x2, x3)] | = | x1 |
[isNatKind(x1)] | = | 0 |
[a__isNatKind(x1)] | = | 0 |
[U103(x1, x2, x3)] | = | 2 · x1 |
[a__U103(x1, x2, x3)] | = | 2 · x1 |
[isNatIListKind(x1)] | = | 0 |
[a__isNatIListKind(x1)] | = | 0 |
[U104(x1, x2, x3)] | = | 2 · x1 |
[a__U104(x1, x2, x3)] | = | 2 · x1 |
[U105(x1, x2)] | = | 2 · x1 |
[a__U105(x1, x2)] | = | 2 · x1 |
[isNat(x1)] | = | 0 |
[a__isNat(x1)] | = | 0 |
[U106(x1)] | = | 2 · x1 |
[a__U106(x1)] | = | 2 · x1 |
[isNatIList(x1)] | = | 0 |
[a__isNatIList(x1)] | = | 0 |
[U11(x1, x2)] | = | x1 |
[a__U11(x1, x2)] | = | x1 |
[U12(x1, x2)] | = | x1 |
[a__U12(x1, x2)] | = | x1 |
[U111(x1, x2, x3)] | = | 2 + 2 · x1 + x2 + 2 · x3 |
[a__U111(x1, x2, x3)] | = | 2 + 2 · x1 + x2 + 2 · x3 |
[U112(x1, x2, x3)] | = | 2 + x1 + x2 + x3 |
[a__U112(x1, x2, x3)] | = | 2 + x1 + x2 + x3 |
[U113(x1, x2, x3)] | = | 2 + x1 + x2 + x3 |
[a__U113(x1, x2, x3)] | = | 2 + x1 + x2 + x3 |
[U114(x1, x2)] | = | 2 + x1 + x2 |
[a__U114(x1, x2)] | = | 2 + x1 + x2 |
[length(x1)] | = | 2 + x1 |
[a__length(x1)] | = | 2 + x1 |
[U13(x1)] | = | 2 · x1 |
[a__U13(x1)] | = | 2 · x1 |
[isNatList(x1)] | = | 0 |
[a__isNatList(x1)] | = | 0 |
[U121(x1, x2)] | = | 0 |
[a__U121(x1, x2)] | = | -2 |
[U122(x1)] | = | 0 |
[a__U122(x1)] | = | -2 |
[U131(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[a__U131(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U132(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[a__U132(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U133(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[a__U133(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U134(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[a__U134(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U135(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[a__U135(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[U136(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[a__U136(x1,...,x4)] | = | 2 + x2 + 2 · x4 |
[take(x1, x2)] | = | 2 + x2 |
[a__take(x1, x2)] | = | 2 + x2 |
[U21(x1, x2)] | = | x1 |
[a__U21(x1, x2)] | = | x1 |
[U22(x1, x2)] | = | 2 · x1 |
[a__U22(x1, x2)] | = | 2 · x1 |
[U23(x1)] | = | 2 · x1 |
[a__U23(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | x1 |
[a__U31(x1, x2)] | = | x1 |
[U32(x1, x2)] | = | 2 · x1 |
[a__U32(x1, x2)] | = | 2 · x1 |
[U33(x1)] | = | 2 · x1 |
[a__U33(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | x1 |
[a__U41(x1, x2, x3)] | = | x1 |
[U42(x1, x2, x3)] | = | x1 |
[a__U42(x1, x2, x3)] | = | x1 |
[U43(x1, x2, x3)] | = | 2 · x1 |
[a__U43(x1, x2, x3)] | = | 2 · x1 |
[U44(x1, x2, x3)] | = | 2 · x1 |
[a__U44(x1, x2, x3)] | = | 2 · x1 |
[U45(x1, x2)] | = | x1 |
[a__U45(x1, x2)] | = | x1 |
[U46(x1)] | = | 2 · x1 |
[a__U46(x1)] | = | 2 · x1 |
[U51(x1, x2)] | = | x1 |
[a__U51(x1, x2)] | = | x1 |
[U52(x1)] | = | 2 · x1 |
[a__U52(x1)] | = | 2 · x1 |
[U61(x1, x2)] | = | 2 · x1 |
[a__U61(x1, x2)] | = | 2 · x1 |
[U62(x1)] | = | x1 |
[a__U62(x1)] | = | x1 |
[U71(x1)] | = | x1 |
[a__U71(x1)] | = | x1 |
[U81(x1)] | = | 2 · x1 |
[a__U81(x1)] | = | 2 · x1 |
[U91(x1, x2, x3)] | = | 2 · x1 |
[a__U91(x1, x2, x3)] | = | 2 · x1 |
[U92(x1, x2, x3)] | = | 2 · x1 |
[a__U92(x1, x2, x3)] | = | 2 · x1 |
[U93(x1, x2, x3)] | = | x1 |
[a__U93(x1, x2, x3)] | = | x1 |
[U94(x1, x2, x3)] | = | x1 |
[a__U94(x1, x2, x3)] | = | x1 |
[U95(x1, x2)] | = | 2 · x1 |
[a__U95(x1, x2)] | = | 2 · x1 |
[U96(x1)] | = | 2 · x1 |
[a__U96(x1)] | = | 2 · x1 |
[cons(x1, x2)] | = | 2 · x1 + x2 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[nil] | = | 0 |
[mark#(x1)] | = | x1 |
mark#(U111(X1,X2,X3)) | → | a__U111#(mark(X1),X2,X3) | (292) |
mark#(U111(X1,X2,X3)) | → | mark#(X1) | (293) |
mark#(U112(X1,X2,X3)) | → | a__U112#(mark(X1),X2,X3) | (294) |
mark#(U112(X1,X2,X3)) | → | mark#(X1) | (295) |
mark#(U113(X1,X2,X3)) | → | a__U113#(mark(X1),X2,X3) | (296) |
mark#(U113(X1,X2,X3)) | → | mark#(X1) | (297) |
mark#(U114(X1,X2)) | → | a__U114#(mark(X1),X2) | (298) |
mark#(U114(X1,X2)) | → | mark#(X1) | (299) |
mark#(length(X)) | → | a__length#(mark(X)) | (300) |
mark#(length(X)) | → | mark#(X) | (301) |
The dependency pairs are split into 2 components.
a__U114#(tt,L) | → | a__length#(mark(L)) | (196) |
a__length#(cons(N,L)) | → | a__U111#(a__isNatList(L),L,N) | (265) |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (190) |
a__U112#(tt,L,N) | → | a__U113#(a__isNat(N),L,N) | (192) |
a__U113#(tt,L,N) | → | a__U114#(a__isNatKind(N),L) | (194) |
[a__length#(x1)] | = | 2 · x1 |
[mark(x1)] | = | x1 |
[zeros] | = | 0 |
[a__zeros] | = | 0 |
[U101(x1, x2, x3)] | = | 2 · x2 |
[a__U101(x1, x2, x3)] | = | 2 · x2 |
[U102(x1, x2, x3)] | = | 2 · x2 |
[a__U102(x1, x2, x3)] | = | 2 · x2 |
[isNatKind(x1)] | = | 2 |
[a__isNatKind(x1)] | = | 2 |
[U103(x1, x2, x3)] | = | 2 · x2 |
[a__U103(x1, x2, x3)] | = | 2 · x2 |
[isNatIListKind(x1)] | = | 1 |
[a__isNatIListKind(x1)] | = | 1 |
[U104(x1, x2, x3)] | = | 2 · x2 |
[a__U104(x1, x2, x3)] | = | 2 · x2 |
[U105(x1, x2)] | = | x1 |
[a__U105(x1, x2)] | = | x1 |
[isNat(x1)] | = | 2 · x1 |
[a__isNat(x1)] | = | 2 · x1 |
[U106(x1)] | = | 1 |
[a__U106(x1)] | = | 1 |
[isNatIList(x1)] | = | 2 |
[a__isNatIList(x1)] | = | 2 |
[U11(x1, x2)] | = | 2 · x2 |
[a__U11(x1, x2)] | = | 2 · x2 |
[U12(x1, x2)] | = | 2 · x2 |
[a__U12(x1, x2)] | = | 2 · x2 |
[U111(x1, x2, x3)] | = | 2 · x2 |
[a__U111(x1, x2, x3)] | = | 2 · x2 |
[U112(x1, x2, x3)] | = | 2 · x2 |
[a__U112(x1, x2, x3)] | = | 2 · x2 |
[U113(x1, x2, x3)] | = | 2 · x2 |
[a__U113(x1, x2, x3)] | = | 2 · x2 |
[U114(x1, x2)] | = | 2 · x2 |
[a__U114(x1, x2)] | = | 2 · x2 |
[length(x1)] | = | x1 |
[a__length(x1)] | = | x1 |
[U13(x1)] | = | x1 |
[a__U13(x1)] | = | x1 |
[isNatList(x1)] | = | 2 · x1 |
[a__isNatList(x1)] | = | 2 · x1 |
[U121(x1, x2)] | = | 2 |
[a__U121(x1, x2)] | = | 2 |
[U122(x1)] | = | 1 + x1 |
[a__U122(x1)] | = | 1 + x1 |
[U131(x1,...,x4)] | = | 2 · x3 |
[a__U131(x1,...,x4)] | = | 2 · x3 |
[U132(x1,...,x4)] | = | 2 · x3 |
[a__U132(x1,...,x4)] | = | 2 · x3 |
[U133(x1,...,x4)] | = | 2 · x3 |
[a__U133(x1,...,x4)] | = | 2 · x3 |
[U134(x1,...,x4)] | = | 2 · x3 |
[a__U134(x1,...,x4)] | = | 2 · x3 |
[U135(x1,...,x4)] | = | 2 · x3 |
[a__U135(x1,...,x4)] | = | 2 · x3 |
[U136(x1,...,x4)] | = | 2 · x3 |
[a__U136(x1,...,x4)] | = | 2 · x3 |
[take(x1, x2)] | = | x1 |
[a__take(x1, x2)] | = | x1 |
[U21(x1, x2)] | = | 2 · x2 |
[a__U21(x1, x2)] | = | 2 · x2 |
[U22(x1, x2)] | = | 2 · x2 |
[a__U22(x1, x2)] | = | 2 · x2 |
[U23(x1)] | = | x1 |
[a__U23(x1)] | = | x1 |
[U31(x1, x2)] | = | 1 |
[a__U31(x1, x2)] | = | 1 |
[U32(x1, x2)] | = | 1 |
[a__U32(x1, x2)] | = | 1 |
[U33(x1)] | = | 1 |
[a__U33(x1)] | = | 1 |
[U41(x1, x2, x3)] | = | 2 |
[a__U41(x1, x2, x3)] | = | 2 |
[U42(x1, x2, x3)] | = | 2 |
[a__U42(x1, x2, x3)] | = | 2 |
[U43(x1, x2, x3)] | = | 2 |
[a__U43(x1, x2, x3)] | = | 2 |
[U44(x1, x2, x3)] | = | 2 |
[a__U44(x1, x2, x3)] | = | 2 |
[U45(x1, x2)] | = | 2 |
[a__U45(x1, x2)] | = | 2 |
[U46(x1)] | = | 2 |
[a__U46(x1)] | = | 2 |
[U51(x1, x2)] | = | 1 |
[a__U51(x1, x2)] | = | 1 |
[U52(x1)] | = | 1 |
[a__U52(x1)] | = | 1 |
[U61(x1, x2)] | = | 1 |
[a__U61(x1, x2)] | = | 1 |
[U62(x1)] | = | 1 |
[a__U62(x1)] | = | 1 |
[U71(x1)] | = | 1 |
[a__U71(x1)] | = | 1 |
[U81(x1)] | = | 1 |
[a__U81(x1)] | = | 1 |
[U91(x1, x2, x3)] | = | 2 · x3 |
[a__U91(x1, x2, x3)] | = | 2 · x3 |
[U92(x1, x2, x3)] | = | 2 · x3 |
[a__U92(x1, x2, x3)] | = | 2 · x3 |
[U93(x1, x2, x3)] | = | 2 · x3 |
[a__U93(x1, x2, x3)] | = | 2 · x3 |
[U94(x1, x2, x3)] | = | 2 · x3 |
[a__U94(x1, x2, x3)] | = | 2 · x3 |
[U95(x1, x2)] | = | 2 · x2 |
[a__U95(x1, x2)] | = | 2 · x2 |
[U96(x1)] | = | x1 |
[a__U96(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x2 |
[0] | = | 2 |
[tt] | = | 1 |
[s(x1)] | = | 2 · x1 |
[nil] | = | 2 |
[a__U111#(x1, x2, x3)] | = | x1 + 2 · x2 |
[a__U113#(x1, x2, x3)] | = | 2 · x2 |
[a__U112#(x1, x2, x3)] | = | 2 · x2 |
[a__U114#(x1, x2)] | = | 2 · x2 |
a__U111#(tt,L,N) | → | a__U112#(a__isNatIListKind(L),L,N) | (190) |
The dependency pairs are split into 0 components.
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (273) |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (275) |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (278) |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (281) |
mark#(U105(X1,X2)) | → | mark#(X1) | (283) |
mark#(U106(X)) | → | mark#(X) | (286) |
mark#(U11(X1,X2)) | → | mark#(X1) | (289) |
mark#(U12(X1,X2)) | → | mark#(X1) | (291) |
mark#(U13(X)) | → | mark#(X) | (303) |
mark#(U21(X1,X2)) | → | mark#(X1) | (325) |
mark#(U22(X1,X2)) | → | mark#(X1) | (327) |
mark#(U23(X)) | → | mark#(X) | (329) |
mark#(U31(X1,X2)) | → | mark#(X1) | (331) |
mark#(U32(X1,X2)) | → | mark#(X1) | (333) |
mark#(U33(X)) | → | mark#(X) | (335) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (337) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (339) |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (341) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (343) |
mark#(U45(X1,X2)) | → | mark#(X1) | (345) |
mark#(U46(X)) | → | mark#(X) | (347) |
mark#(U51(X1,X2)) | → | mark#(X1) | (349) |
mark#(U52(X)) | → | mark#(X) | (351) |
mark#(U61(X1,X2)) | → | mark#(X1) | (353) |
mark#(U62(X)) | → | mark#(X) | (355) |
mark#(U71(X)) | → | mark#(X) | (357) |
mark#(U81(X)) | → | mark#(X) | (359) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (361) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (363) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (365) |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (367) |
mark#(U95(X1,X2)) | → | mark#(X1) | (369) |
mark#(U96(X)) | → | mark#(X) | (371) |
mark#(cons(X1,X2)) | → | mark#(X1) | (372) |
mark#(s(X)) | → | mark#(X) | (373) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
mark#(U101(X1,X2,X3)) | → | mark#(X1) | (273) |
1 | > | 1 | |
mark#(U102(X1,X2,X3)) | → | mark#(X1) | (275) |
1 | > | 1 | |
mark#(U103(X1,X2,X3)) | → | mark#(X1) | (278) |
1 | > | 1 | |
mark#(U104(X1,X2,X3)) | → | mark#(X1) | (281) |
1 | > | 1 | |
mark#(U105(X1,X2)) | → | mark#(X1) | (283) |
1 | > | 1 | |
mark#(U106(X)) | → | mark#(X) | (286) |
1 | > | 1 | |
mark#(U11(X1,X2)) | → | mark#(X1) | (289) |
1 | > | 1 | |
mark#(U12(X1,X2)) | → | mark#(X1) | (291) |
1 | > | 1 | |
mark#(U13(X)) | → | mark#(X) | (303) |
1 | > | 1 | |
mark#(U21(X1,X2)) | → | mark#(X1) | (325) |
1 | > | 1 | |
mark#(U22(X1,X2)) | → | mark#(X1) | (327) |
1 | > | 1 | |
mark#(U23(X)) | → | mark#(X) | (329) |
1 | > | 1 | |
mark#(U31(X1,X2)) | → | mark#(X1) | (331) |
1 | > | 1 | |
mark#(U32(X1,X2)) | → | mark#(X1) | (333) |
1 | > | 1 | |
mark#(U33(X)) | → | mark#(X) | (335) |
1 | > | 1 | |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (337) |
1 | > | 1 | |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (339) |
1 | > | 1 | |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (341) |
1 | > | 1 | |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (343) |
1 | > | 1 | |
mark#(U45(X1,X2)) | → | mark#(X1) | (345) |
1 | > | 1 | |
mark#(U46(X)) | → | mark#(X) | (347) |
1 | > | 1 | |
mark#(U51(X1,X2)) | → | mark#(X1) | (349) |
1 | > | 1 | |
mark#(U52(X)) | → | mark#(X) | (351) |
1 | > | 1 | |
mark#(U61(X1,X2)) | → | mark#(X1) | (353) |
1 | > | 1 | |
mark#(U62(X)) | → | mark#(X) | (355) |
1 | > | 1 | |
mark#(U71(X)) | → | mark#(X) | (357) |
1 | > | 1 | |
mark#(U81(X)) | → | mark#(X) | (359) |
1 | > | 1 | |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (361) |
1 | > | 1 | |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (363) |
1 | > | 1 | |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (365) |
1 | > | 1 | |
mark#(U94(X1,X2,X3)) | → | mark#(X1) | (367) |
1 | > | 1 | |
mark#(U95(X1,X2)) | → | mark#(X1) | (369) |
1 | > | 1 | |
mark#(U96(X)) | → | mark#(X) | (371) |
1 | > | 1 | |
mark#(cons(X1,X2)) | → | mark#(X1) | (372) |
1 | > | 1 | |
mark#(s(X)) | → | mark#(X) | (373) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U102#(tt,V1,V2) | → | a__U103#(a__isNatIListKind(V2),V1,V2) | (180) |
a__U103#(tt,V1,V2) | → | a__U104#(a__isNatIListKind(V2),V1,V2) | (182) |
a__U104#(tt,V1,V2) | → | a__U105#(a__isNat(V1),V2) | (184) |
a__U105#(tt,V2) | → | a__isNatIList#(V2) | (187) |
a__isNatIList#(V) | → | a__U31#(a__isNatIListKind(V),V) | (249) |
a__U31#(tt,V) | → | a__U32#(a__isNatIListKind(V),V) | (217) |
a__U32#(tt,V) | → | a__isNatList#(V) | (220) |
a__isNatList#(cons(V1,V2)) | → | a__U91#(a__isNatKind(V1),V1,V2) | (261) |
a__U91#(tt,V1,V2) | → | a__U92#(a__isNatKind(V1),V1,V2) | (235) |
a__U92#(tt,V1,V2) | → | a__U93#(a__isNatIListKind(V2),V1,V2) | (237) |
a__U93#(tt,V1,V2) | → | a__U94#(a__isNatIListKind(V2),V1,V2) | (239) |
a__U94#(tt,V1,V2) | → | a__U95#(a__isNat(V1),V2) | (241) |
a__U95#(tt,V2) | → | a__isNatList#(V2) | (244) |
a__isNatList#(take(V1,V2)) | → | a__U101#(a__isNatKind(V1),V1,V2) | (263) |
a__U101#(tt,V1,V2) | → | a__U102#(a__isNatKind(V1),V1,V2) | (178) |
a__U94#(tt,V1,V2) | → | a__isNat#(V1) | (242) |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (245) |
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (188) |
a__U12#(tt,V1) | → | a__isNatList#(V1) | (199) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (247) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (213) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (216) |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (251) |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (221) |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (223) |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (225) |
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (227) |
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (230) |
a__U44#(tt,V1,V2) | → | a__isNat#(V1) | (228) |
a__U104#(tt,V1,V2) | → | a__isNat#(V1) | (185) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNat(0) | → | tt | (47) |
a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1),V1) | (48) |
a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1),V1) | (49) |
a__isNat(X) | → | isNat(X) | (133) |
a__isNatKind(0) | → | tt | (57) |
a__isNatKind(length(V1)) | → | a__U71(a__isNatIListKind(V1)) | (58) |
a__isNatKind(s(V1)) | → | a__U81(a__isNatKind(V1)) | (59) |
a__isNatKind(X) | → | isNatKind(X) | (128) |
a__U21(tt,V1) | → | a__U22(a__isNatKind(V1),V1) | (23) |
a__U21(X1,X2) | → | U21(X1,X2) | (154) |
a__U22(tt,V1) | → | a__U23(a__isNat(V1)) | (24) |
a__U22(X1,X2) | → | U22(X1,X2) | (155) |
a__U23(tt) | → | tt | (25) |
a__U23(X) | → | U23(X) | (156) |
a__U81(tt) | → | tt | (40) |
a__U81(X) | → | U81(X) | (171) |
a__isNatIListKind(nil) | → | tt | (53) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__U71(tt) | → | tt | (39) |
a__U71(X) | → | U71(X) | (170) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__U62(tt) | → | tt | (38) |
a__U62(X) | → | U62(X) | (169) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__U52(tt) | → | tt | (36) |
a__U52(X) | → | U52(X) | (167) |
a__U11(tt,V1) | → | a__U12(a__isNatIListKind(V1),V1) | (8) |
a__U11(X1,X2) | → | U11(X1,X2) | (136) |
a__U12(tt,V1) | → | a__U13(a__isNatList(V1)) | (13) |
a__U12(X1,X2) | → | U12(X1,X2) | (137) |
a__isNatList(nil) | → | tt | (60) |
a__isNatList(cons(V1,V2)) | → | a__U91(a__isNatKind(V1),V1,V2) | (61) |
a__isNatList(take(V1,V2)) | → | a__U101(a__isNatKind(V1),V1,V2) | (62) |
a__isNatList(X) | → | isNatList(X) | (144) |
a__U13(tt) | → | tt | (16) |
a__U13(X) | → | U13(X) | (143) |
a__U101(tt,V1,V2) | → | a__U102(a__isNatKind(V1),V1,V2) | (2) |
a__U101(X1,X2,X3) | → | U101(X1,X2,X3) | (126) |
a__U102(tt,V1,V2) | → | a__U103(a__isNatIListKind(V2),V1,V2) | (3) |
a__U102(X1,X2,X3) | → | U102(X1,X2,X3) | (127) |
a__U103(tt,V1,V2) | → | a__U104(a__isNatIListKind(V2),V1,V2) | (4) |
a__U103(X1,X2,X3) | → | U103(X1,X2,X3) | (129) |
a__U104(tt,V1,V2) | → | a__U105(a__isNat(V1),V2) | (5) |
a__U104(X1,X2,X3) | → | U104(X1,X2,X3) | (131) |
a__U105(tt,V2) | → | a__U106(a__isNatIList(V2)) | (6) |
a__U105(X1,X2) | → | U105(X1,X2) | (132) |
a__isNatIList(V) | → | a__U31(a__isNatIListKind(V),V) | (50) |
a__isNatIList(zeros) | → | tt | (51) |
a__isNatIList(cons(V1,V2)) | → | a__U41(a__isNatKind(V1),V1,V2) | (52) |
a__isNatIList(X) | → | isNatIList(X) | (135) |
a__U106(tt) | → | tt | (7) |
a__U106(X) | → | U106(X) | (134) |
a__U41(tt,V1,V2) | → | a__U42(a__isNatKind(V1),V1,V2) | (29) |
a__U41(X1,X2,X3) | → | U41(X1,X2,X3) | (160) |
a__U42(tt,V1,V2) | → | a__U43(a__isNatIListKind(V2),V1,V2) | (30) |
a__U42(X1,X2,X3) | → | U42(X1,X2,X3) | (161) |
a__U43(tt,V1,V2) | → | a__U44(a__isNatIListKind(V2),V1,V2) | (31) |
a__U43(X1,X2,X3) | → | U43(X1,X2,X3) | (162) |
a__U44(tt,V1,V2) | → | a__U45(a__isNat(V1),V2) | (32) |
a__U44(X1,X2,X3) | → | U44(X1,X2,X3) | (163) |
a__U45(tt,V2) | → | a__U46(a__isNatIList(V2)) | (33) |
a__U45(X1,X2) | → | U45(X1,X2) | (164) |
a__U46(tt) | → | tt | (34) |
a__U46(X) | → | U46(X) | (165) |
a__U31(tt,V) | → | a__U32(a__isNatIListKind(V),V) | (26) |
a__U31(X1,X2) | → | U31(X1,X2) | (157) |
a__U32(tt,V) | → | a__U33(a__isNatList(V)) | (27) |
a__U32(X1,X2) | → | U32(X1,X2) | (158) |
a__U33(tt) | → | tt | (28) |
a__U33(X) | → | U33(X) | (159) |
a__U91(tt,V1,V2) | → | a__U92(a__isNatKind(V1),V1,V2) | (41) |
a__U91(X1,X2,X3) | → | U91(X1,X2,X3) | (172) |
a__U92(tt,V1,V2) | → | a__U93(a__isNatIListKind(V2),V1,V2) | (42) |
a__U92(X1,X2,X3) | → | U92(X1,X2,X3) | (173) |
a__U93(tt,V1,V2) | → | a__U94(a__isNatIListKind(V2),V1,V2) | (43) |
a__U93(X1,X2,X3) | → | U93(X1,X2,X3) | (174) |
a__U94(tt,V1,V2) | → | a__U95(a__isNat(V1),V2) | (44) |
a__U94(X1,X2,X3) | → | U94(X1,X2,X3) | (175) |
a__U95(tt,V2) | → | a__U96(a__isNatList(V2)) | (45) |
a__U95(X1,X2) | → | U95(X1,X2) | (176) |
a__U96(tt) | → | tt | (46) |
a__U96(X) | → | U96(X) | (177) |
We restrict the innermost strategy to the following left hand sides.
a__isNatIList(x0) |
a__U101(x0,x1,x2) |
a__U102(x0,x1,x2) |
a__isNatKind(x0) |
a__U103(x0,x1,x2) |
a__isNatIListKind(x0) |
a__U104(x0,x1,x2) |
a__U105(x0,x1) |
a__isNat(x0) |
a__U106(x0) |
a__U11(x0,x1) |
a__U12(x0,x1) |
a__U13(x0) |
a__isNatList(x0) |
a__U21(x0,x1) |
a__U22(x0,x1) |
a__U23(x0) |
a__U31(x0,x1) |
a__U32(x0,x1) |
a__U33(x0) |
a__U41(x0,x1,x2) |
a__U42(x0,x1,x2) |
a__U43(x0,x1,x2) |
a__U44(x0,x1,x2) |
a__U45(x0,x1) |
a__U46(x0) |
a__U51(x0,x1) |
a__U52(x0) |
a__U61(x0,x1) |
a__U62(x0) |
a__U71(x0) |
a__U81(x0) |
a__U91(x0,x1,x2) |
a__U92(x0,x1,x2) |
a__U93(x0,x1,x2) |
a__U94(x0,x1,x2) |
a__U95(x0,x1) |
a__U96(x0) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
a__U103#(tt,V1,V2) | → | a__U104#(a__isNatIListKind(V2),V1,V2) | (182) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U101#(tt,V1,V2) | → | a__U102#(a__isNatKind(V1),V1,V2) | (178) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U102#(tt,V1,V2) | → | a__U103#(a__isNatIListKind(V2),V1,V2) | (180) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U105#(tt,V2) | → | a__isNatIList#(V2) | (187) |
2 | ≥ | 1 | |
a__U104#(tt,V1,V2) | → | a__U105#(a__isNat(V1),V2) | (184) |
3 | ≥ | 2 | |
a__U104#(tt,V1,V2) | → | a__isNat#(V1) | (185) |
2 | ≥ | 1 | |
a__U31#(tt,V) | → | a__U32#(a__isNatIListKind(V),V) | (217) |
2 | ≥ | 2 | |
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (230) |
2 | ≥ | 1 | |
a__isNatIList#(V) | → | a__U31#(a__isNatIListKind(V),V) | (249) |
1 | ≥ | 2 | |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (251) |
1 | > | 2 | |
1 | > | 3 | |
a__U32#(tt,V) | → | a__isNatList#(V) | (220) |
2 | ≥ | 1 | |
a__U91#(tt,V1,V2) | → | a__U92#(a__isNatKind(V1),V1,V2) | (235) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__isNatList#(cons(V1,V2)) | → | a__U91#(a__isNatKind(V1),V1,V2) | (261) |
1 | > | 2 | |
1 | > | 3 | |
a__isNatList#(take(V1,V2)) | → | a__U101#(a__isNatKind(V1),V1,V2) | (263) |
1 | > | 2 | |
1 | > | 3 | |
a__U92#(tt,V1,V2) | → | a__U93#(a__isNatIListKind(V2),V1,V2) | (237) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U93#(tt,V1,V2) | → | a__U94#(a__isNatIListKind(V2),V1,V2) | (239) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U95#(tt,V2) | → | a__isNatList#(V2) | (244) |
2 | ≥ | 1 | |
a__U12#(tt,V1) | → | a__isNatList#(V1) | (199) |
2 | ≥ | 1 | |
a__U94#(tt,V1,V2) | → | a__U95#(a__isNat(V1),V2) | (241) |
3 | ≥ | 2 | |
a__U94#(tt,V1,V2) | → | a__isNat#(V1) | (242) |
2 | ≥ | 1 | |
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (188) |
2 | ≥ | 2 | |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (245) |
1 | > | 2 | |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (247) |
1 | > | 2 | |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (213) |
2 | ≥ | 2 | |
a__U22#(tt,V1) | → | a__isNat#(V1) | (216) |
2 | ≥ | 1 | |
a__U44#(tt,V1,V2) | → | a__isNat#(V1) | (228) |
2 | ≥ | 1 | |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (221) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (223) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (225) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (227) |
3 | ≥ | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U51#(tt,V2) | → | a__isNatIListKind#(V2) | (232) |
a__isNatIListKind#(cons(V1,V2)) | → | a__U51#(a__isNatKind(V1),V2) | (253) |
a__isNatIListKind#(cons(V1,V2)) | → | a__isNatKind#(V1) | (254) |
a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | (258) |
a__isNatIListKind#(take(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (255) |
a__U61#(tt,V2) | → | a__isNatIListKind#(V2) | (234) |
a__isNatIListKind#(take(V1,V2)) | → | a__isNatKind#(V1) | (256) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (260) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNatKind(0) | → | tt | (57) |
a__isNatKind(length(V1)) | → | a__U71(a__isNatIListKind(V1)) | (58) |
a__isNatKind(s(V1)) | → | a__U81(a__isNatKind(V1)) | (59) |
a__isNatKind(X) | → | isNatKind(X) | (128) |
a__U81(tt) | → | tt | (40) |
a__U81(X) | → | U81(X) | (171) |
a__isNatIListKind(nil) | → | tt | (53) |
a__isNatIListKind(zeros) | → | tt | (54) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (55) |
a__isNatIListKind(take(V1,V2)) | → | a__U61(a__isNatKind(V1),V2) | (56) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (130) |
a__U71(tt) | → | tt | (39) |
a__U71(X) | → | U71(X) | (170) |
a__U61(tt,V2) | → | a__U62(a__isNatIListKind(V2)) | (37) |
a__U61(X1,X2) | → | U61(X1,X2) | (168) |
a__U62(tt) | → | tt | (38) |
a__U62(X) | → | U62(X) | (169) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (35) |
a__U51(X1,X2) | → | U51(X1,X2) | (166) |
a__U52(tt) | → | tt | (36) |
a__U52(X) | → | U52(X) | (167) |
We restrict the innermost strategy to the following left hand sides.
a__isNatKind(x0) |
a__isNatIListKind(x0) |
a__U51(x0,x1) |
a__U52(x0) |
a__U61(x0,x1) |
a__U62(x0) |
a__U71(x0) |
a__U81(x0) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
a__isNatIListKind#(cons(V1,V2)) | → | a__U51#(a__isNatKind(V1),V2) | (253) |
1 | > | 2 | |
a__U51#(tt,V2) | → | a__isNatIListKind#(V2) | (232) |
2 | ≥ | 1 | |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (260) |
1 | > | 1 | |
a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | (258) |
1 | > | 1 | |
a__U61#(tt,V2) | → | a__isNatIListKind#(V2) | (234) |
2 | ≥ | 1 | |
a__isNatIListKind#(take(V1,V2)) | → | a__U61#(a__isNatKind(V1),V2) | (255) |
1 | > | 2 | |
a__isNatIListKind#(cons(V1,V2)) | → | a__isNatKind#(V1) | (254) |
1 | > | 1 | |
a__isNatIListKind#(take(V1,V2)) | → | a__isNatKind#(V1) | (256) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.