The rewrite relation of the following TRS is considered.
There are 123 ruless (increase limit for explicit display).
The evaluation strategy is innermost.There are 128 ruless (increase limit for explicit display).
The dependency pairs are split into 4 components.
mark#(U11(X1,X2)) | → | mark#(X1) | (186) |
mark#(U12(X1,X2)) | → | mark#(X1) | (188) |
mark#(U13(X)) | → | mark#(X) | (191) |
mark#(U21(X1,X2)) | → | mark#(X1) | (194) |
mark#(U22(X1,X2)) | → | mark#(X1) | (196) |
mark#(U23(X)) | → | mark#(X) | (199) |
mark#(U31(X1,X2)) | → | mark#(X1) | (202) |
mark#(U32(X1,X2)) | → | mark#(X1) | (204) |
mark#(U33(X)) | → | mark#(X) | (206) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (208) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (210) |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (212) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (214) |
mark#(U45(X1,X2)) | → | mark#(X1) | (216) |
mark#(U46(X)) | → | mark#(X) | (218) |
mark#(U51(X1,X2)) | → | mark#(X1) | (221) |
mark#(U52(X)) | → | mark#(X) | (223) |
mark#(U61(X)) | → | mark#(X) | (225) |
mark#(U71(X)) | → | mark#(X) | (227) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (229) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (231) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (233) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (235) |
mark#(U85(X1,X2)) | → | mark#(X1) | (237) |
mark#(U86(X)) | → | mark#(X) | (239) |
mark#(U91(X1,X2,X3)) | → | a__U91#(mark(X1),X2,X3) | (240) |
a__U91#(tt,L,N) | → | a__U92#(a__isNatIListKind(L),L,N) | (158) |
a__U92#(tt,L,N) | → | a__U93#(a__isNat(N),L,N) | (160) |
a__U93#(tt,L,N) | → | a__U94#(a__isNatKind(N),L) | (162) |
a__U94#(tt,L) | → | a__length#(mark(L)) | (164) |
a__length#(cons(N,L)) | → | a__U91#(a__isNatList(L),L,N) | (182) |
a__U94#(tt,L) | → | mark#(L) | (165) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (241) |
mark#(U92(X1,X2,X3)) | → | a__U92#(mark(X1),X2,X3) | (242) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (243) |
mark#(U93(X1,X2,X3)) | → | a__U93#(mark(X1),X2,X3) | (244) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (245) |
mark#(U94(X1,X2)) | → | a__U94#(mark(X1),X2) | (246) |
mark#(U94(X1,X2)) | → | mark#(X1) | (247) |
mark#(length(X)) | → | a__length#(mark(X)) | (248) |
mark#(length(X)) | → | mark#(X) | (249) |
mark#(cons(X1,X2)) | → | mark#(X1) | (250) |
mark#(s(X)) | → | mark#(X) | (251) |
[a__length#(x1)] | = | -1 + x1 |
[a__U91#(x1, x2, x3)] | = | 1 + 2 · x2 + x3 |
[a__U92#(x1, x2, x3)] | = | 1 + x1 + 2 · x2 |
[a__U93#(x1, x2, x3)] | = | 1 + 2 · x2 |
[a__U94#(x1, x2)] | = | 1 + 2 · x2 |
[mark(x1)] | = | 2 + x1 |
[zeros] | = | 0 |
[a__zeros] | = | 2 |
[U11(x1, x2)] | = | x1 |
[a__U11(x1, x2)] | = | x1 |
[U12(x1, x2)] | = | x1 |
[a__U12(x1, x2)] | = | x1 |
[isNatIListKind(x1)] | = | 0 |
[a__isNatIListKind(x1)] | = | 0 |
[U13(x1)] | = | x1 |
[a__U13(x1)] | = | x1 |
[isNatList(x1)] | = | 0 |
[a__isNatList(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 |
[a__U21(x1, x2)] | = | x1 |
[U22(x1, x2)] | = | x1 |
[a__U22(x1, x2)] | = | x1 |
[isNatKind(x1)] | = | 0 |
[a__isNatKind(x1)] | = | 0 |
[U23(x1)] | = | x1 |
[a__U23(x1)] | = | x1 |
[isNat(x1)] | = | 0 |
[a__isNat(x1)] | = | 0 |
[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)] | = | x1 |
[a__U41(x1, x2, x3)] | = | 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)] | = | x1 |
[a__U45(x1, x2)] | = | x1 |
[U46(x1)] | = | x1 |
[a__U46(x1)] | = | x1 |
[isNatIList(x1)] | = | 0 |
[a__isNatIList(x1)] | = | 0 |
[U51(x1, x2)] | = | x1 |
[a__U51(x1, x2)] | = | x1 |
[U52(x1)] | = | x1 |
[a__U52(x1)] | = | x1 |
[U61(x1)] | = | x1 |
[a__U61(x1)] | = | x1 |
[U71(x1)] | = | x1 |
[a__U71(x1)] | = | x1 |
[U81(x1, x2, x3)] | = | x1 |
[a__U81(x1, x2, x3)] | = | x1 |
[U82(x1, x2, x3)] | = | x1 |
[a__U82(x1, x2, x3)] | = | x1 |
[U83(x1, x2, x3)] | = | x1 |
[a__U83(x1, x2, x3)] | = | x1 |
[U84(x1, x2, x3)] | = | x1 |
[a__U84(x1, x2, x3)] | = | x1 |
[U85(x1, x2)] | = | x1 |
[a__U85(x1, x2)] | = | x1 |
[U86(x1)] | = | x1 |
[a__U86(x1)] | = | x1 |
[U91(x1, x2, x3)] | = | 2 + x1 + 2 · x2 + x3 |
[a__U91(x1, x2, x3)] | = | 2 + x1 + 2 · x2 + x3 |
[U92(x1, x2, x3)] | = | 2 + x1 + 2 · x2 |
[a__U92(x1, x2, x3)] | = | 2 + x1 + 2 · x2 |
[U93(x1, x2, x3)] | = | 2 + x1 + 2 · x2 |
[a__U93(x1, x2, x3)] | = | 2 + x1 + 2 · x2 |
[U94(x1, x2)] | = | 2 + x1 + 2 · x2 |
[a__U94(x1, x2)] | = | 2 + x1 + 2 · x2 |
[length(x1)] | = | x1 |
[a__length(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 + x1 + 2 · x2 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[nil] | = | 2 |
[mark#(x1)] | = | 1 + 2 · x1 |
mark#(U91(X1,X2,X3)) | → | a__U91#(mark(X1),X2,X3) | (240) |
mark#(U91(X1,X2,X3)) | → | mark#(X1) | (241) |
mark#(U92(X1,X2,X3)) | → | a__U92#(mark(X1),X2,X3) | (242) |
mark#(U92(X1,X2,X3)) | → | mark#(X1) | (243) |
mark#(U93(X1,X2,X3)) | → | a__U93#(mark(X1),X2,X3) | (244) |
mark#(U93(X1,X2,X3)) | → | mark#(X1) | (245) |
mark#(U94(X1,X2)) | → | a__U94#(mark(X1),X2) | (246) |
mark#(U94(X1,X2)) | → | mark#(X1) | (247) |
mark#(cons(X1,X2)) | → | mark#(X1) | (250) |
[a__length#(x1)] | = | 1 + x1 |
[a__U92#(x1, x2, x3)] | = | 1 + 2 · x2 |
[a__U91#(x1, x2, x3)] | = | 1 + 2 · x2 |
[a__U11(x1, x2)] | = | 2 · x1 |
[a__U12(x1, x2)] | = | 2 · x1 |
[a__U83(x1, x2, x3)] | = | 2 · x1 |
[a__U84(x1, x2, x3)] | = | x1 |
[a__U93#(x1, x2, x3)] | = | 1 + 2 · x2 |
[a__U94#(x1, x2)] | = | 1 + 2 · x2 |
[a__U52(x1)] | = | x1 |
[a__U61(x1)] | = | 2 · x1 |
[a__U21(x1, x2)] | = | 2 · x1 |
[a__U22(x1, x2)] | = | 2 · x1 |
[a__U81(x1, x2, x3)] | = | x1 |
[a__U82(x1, x2, x3)] | = | 2 · x1 |
[a__isNatIListKind(x1)] | = | 0 |
[nil] | = | 0 |
[tt] | = | 0 |
[zeros] | = | 0 |
[cons(x1, x2)] | = | 2 · x2 |
[a__U51(x1, x2)] | = | 2 · x1 |
[a__isNatKind(x1)] | = | 0 |
[isNatIListKind(x1)] | = | 0 |
[a__U23(x1)] | = | x1 |
[a__U85(x1, x2)] | = | 2 · x1 |
[a__isNat(x1)] | = | 0 |
[0] | = | 0 |
[length(x1)] | = | 2 + x1 |
[s(x1)] | = | x1 |
[isNat(x1)] | = | 0 |
[a__U71(x1)] | = | x1 |
[isNatKind(x1)] | = | 0 |
[mark(x1)] | = | x1 |
[a__zeros] | = | 0 |
[U11(x1, x2)] | = | 2 · x1 |
[U12(x1, x2)] | = | 2 · x1 |
[U13(x1)] | = | 2 · x1 |
[a__U13(x1)] | = | 2 · x1 |
[isNatList(x1)] | = | 0 |
[a__isNatList(x1)] | = | 0 |
[U21(x1, x2)] | = | 2 · x1 |
[U22(x1, x2)] | = | 2 · x1 |
[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)] | = | 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)] | = | 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 |
[isNatIList(x1)] | = | 0 |
[a__isNatIList(x1)] | = | 0 |
[U51(x1, x2)] | = | 2 · x1 |
[U52(x1)] | = | x1 |
[U61(x1)] | = | 2 · x1 |
[U71(x1)] | = | x1 |
[U81(x1, x2, x3)] | = | x1 |
[U82(x1, x2, x3)] | = | 2 · x1 |
[U83(x1, x2, x3)] | = | 2 · x1 |
[U84(x1, x2, x3)] | = | x1 |
[U85(x1, x2)] | = | 2 · x1 |
[U86(x1)] | = | 2 · x1 |
[a__U86(x1)] | = | 2 · x1 |
[U91(x1, x2, x3)] | = | 2 + 2 · x2 |
[a__U91(x1, x2, x3)] | = | 2 + 2 · x2 |
[U92(x1, x2, x3)] | = | 2 + 2 · x2 |
[a__U92(x1, x2, x3)] | = | 2 + 2 · x2 |
[U93(x1, x2, x3)] | = | 2 + 2 · x2 |
[a__U93(x1, x2, x3)] | = | 2 + 2 · x2 |
[U94(x1, x2)] | = | 2 + 2 · x2 |
[a__U94(x1, x2)] | = | 2 + 2 · x2 |
[a__length(x1)] | = | 2 + x1 |
[mark#(x1)] | = | 2 · x1 |
a__U94#(tt,L) | → | mark#(L) | (165) |
mark#(length(X)) | → | a__length#(mark(X)) | (248) |
mark#(length(X)) | → | mark#(X) | (249) |
The dependency pairs are split into 2 components.
mark#(U12(X1,X2)) | → | mark#(X1) | (188) |
mark#(U11(X1,X2)) | → | mark#(X1) | (186) |
mark#(U13(X)) | → | mark#(X) | (191) |
mark#(U21(X1,X2)) | → | mark#(X1) | (194) |
mark#(U22(X1,X2)) | → | mark#(X1) | (196) |
mark#(U23(X)) | → | mark#(X) | (199) |
mark#(U31(X1,X2)) | → | mark#(X1) | (202) |
mark#(U32(X1,X2)) | → | mark#(X1) | (204) |
mark#(U33(X)) | → | mark#(X) | (206) |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (208) |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (210) |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (212) |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (214) |
mark#(U45(X1,X2)) | → | mark#(X1) | (216) |
mark#(U46(X)) | → | mark#(X) | (218) |
mark#(U51(X1,X2)) | → | mark#(X1) | (221) |
mark#(U52(X)) | → | mark#(X) | (223) |
mark#(U61(X)) | → | mark#(X) | (225) |
mark#(U71(X)) | → | mark#(X) | (227) |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (229) |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (231) |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (233) |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (235) |
mark#(U85(X1,X2)) | → | mark#(X1) | (237) |
mark#(U86(X)) | → | mark#(X) | (239) |
mark#(s(X)) | → | mark#(X) | (251) |
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#(U12(X1,X2)) | → | mark#(X1) | (188) |
1 | > | 1 | |
mark#(U11(X1,X2)) | → | mark#(X1) | (186) |
1 | > | 1 | |
mark#(U13(X)) | → | mark#(X) | (191) |
1 | > | 1 | |
mark#(U21(X1,X2)) | → | mark#(X1) | (194) |
1 | > | 1 | |
mark#(U22(X1,X2)) | → | mark#(X1) | (196) |
1 | > | 1 | |
mark#(U23(X)) | → | mark#(X) | (199) |
1 | > | 1 | |
mark#(U31(X1,X2)) | → | mark#(X1) | (202) |
1 | > | 1 | |
mark#(U32(X1,X2)) | → | mark#(X1) | (204) |
1 | > | 1 | |
mark#(U33(X)) | → | mark#(X) | (206) |
1 | > | 1 | |
mark#(U41(X1,X2,X3)) | → | mark#(X1) | (208) |
1 | > | 1 | |
mark#(U42(X1,X2,X3)) | → | mark#(X1) | (210) |
1 | > | 1 | |
mark#(U43(X1,X2,X3)) | → | mark#(X1) | (212) |
1 | > | 1 | |
mark#(U44(X1,X2,X3)) | → | mark#(X1) | (214) |
1 | > | 1 | |
mark#(U45(X1,X2)) | → | mark#(X1) | (216) |
1 | > | 1 | |
mark#(U46(X)) | → | mark#(X) | (218) |
1 | > | 1 | |
mark#(U51(X1,X2)) | → | mark#(X1) | (221) |
1 | > | 1 | |
mark#(U52(X)) | → | mark#(X) | (223) |
1 | > | 1 | |
mark#(U61(X)) | → | mark#(X) | (225) |
1 | > | 1 | |
mark#(U71(X)) | → | mark#(X) | (227) |
1 | > | 1 | |
mark#(U81(X1,X2,X3)) | → | mark#(X1) | (229) |
1 | > | 1 | |
mark#(U82(X1,X2,X3)) | → | mark#(X1) | (231) |
1 | > | 1 | |
mark#(U83(X1,X2,X3)) | → | mark#(X1) | (233) |
1 | > | 1 | |
mark#(U84(X1,X2,X3)) | → | mark#(X1) | (235) |
1 | > | 1 | |
mark#(U85(X1,X2)) | → | mark#(X1) | (237) |
1 | > | 1 | |
mark#(U86(X)) | → | mark#(X) | (239) |
1 | > | 1 | |
mark#(s(X)) | → | mark#(X) | (251) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U92#(tt,L,N) | → | a__U93#(a__isNat(N),L,N) | (160) |
a__U93#(tt,L,N) | → | a__U94#(a__isNatKind(N),L) | (162) |
a__U94#(tt,L) | → | a__length#(mark(L)) | (164) |
a__length#(cons(N,L)) | → | a__U91#(a__isNatList(L),L,N) | (182) |
a__U91#(tt,L,N) | → | a__U92#(a__isNatIListKind(L),L,N) | (158) |
[a__length#(x1)] | = | 1 + 2 · x1 |
[a__U93#(x1, x2, x3)] | = | 2 + 2 · x2 |
[a__U91#(x1, x2, x3)] | = | 2 · x1 + 2 · x2 |
[a__U23(x1)] | = | 1 |
[a__U85(x1, x2)] | = | x2 |
[a__isNat(x1)] | = | x1 |
[0] | = | 1 |
[tt] | = | 1 |
[length(x1)] | = | 2 |
[a__U11(x1, x2)] | = | 1 |
[a__isNatIListKind(x1)] | = | 2 |
[s(x1)] | = | 1 |
[a__U21(x1, x2)] | = | 1 |
[a__isNatKind(x1)] | = | 2 + 2 · x1 |
[isNat(x1)] | = | x1 |
[a__U94#(x1, x2)] | = | 1 + 2 · x2 |
[a__U22(x1, x2)] | = | 1 |
[a__U81(x1, x2, x3)] | = | 2 · x3 |
[a__U82(x1, x2, x3)] | = | 2 · x3 |
[a__U92#(x1, x2, x3)] | = | 2 + 2 · x2 |
[a__U51(x1, x2)] | = | 2 |
[a__U71(x1)] | = | 1 |
[a__U12(x1, x2)] | = | 1 |
[a__U83(x1, x2, x3)] | = | 2 · x3 |
[a__U84(x1, x2, x3)] | = | x3 |
[a__U61(x1)] | = | 2 + 2 · x1 |
[isNatKind(x1)] | = | 2 + 2 · x1 |
[mark(x1)] | = | x1 |
[zeros] | = | 0 |
[a__zeros] | = | 0 |
[U11(x1, x2)] | = | 1 |
[U12(x1, x2)] | = | 1 |
[isNatIListKind(x1)] | = | 2 |
[U13(x1)] | = | 1 |
[a__U13(x1)] | = | 1 |
[isNatList(x1)] | = | x1 |
[a__isNatList(x1)] | = | x1 |
[U21(x1, x2)] | = | 1 |
[U22(x1, x2)] | = | 1 |
[U23(x1)] | = | 1 |
[U31(x1, x2)] | = | 2 |
[a__U31(x1, x2)] | = | 2 |
[U32(x1, x2)] | = | 1 |
[a__U32(x1, x2)] | = | 1 |
[U33(x1)] | = | 1 |
[a__U33(x1)] | = | 1 |
[U41(x1, x2, x3)] | = | 1 |
[a__U41(x1, x2, x3)] | = | 1 |
[U42(x1, x2, x3)] | = | 1 |
[a__U42(x1, x2, x3)] | = | 1 |
[U43(x1, x2, x3)] | = | 1 |
[a__U43(x1, x2, x3)] | = | 1 |
[U44(x1, x2, x3)] | = | 1 |
[a__U44(x1, x2, x3)] | = | 1 |
[U45(x1, x2)] | = | 1 |
[a__U45(x1, x2)] | = | 1 |
[U46(x1)] | = | 1 |
[a__U46(x1)] | = | 1 |
[isNatIList(x1)] | = | 2 |
[a__isNatIList(x1)] | = | 2 |
[U51(x1, x2)] | = | 2 |
[U52(x1)] | = | 2 |
[a__U52(x1)] | = | 2 |
[U61(x1)] | = | 2 + 2 · x1 |
[U71(x1)] | = | 1 |
[U81(x1, x2, x3)] | = | 2 · x3 |
[U82(x1, x2, x3)] | = | 2 · x3 |
[U83(x1, x2, x3)] | = | 2 · x3 |
[U84(x1, x2, x3)] | = | x3 |
[U85(x1, x2)] | = | x2 |
[U86(x1)] | = | x1 |
[a__U86(x1)] | = | x1 |
[U91(x1, x2, x3)] | = | 2 |
[a__U91(x1, x2, x3)] | = | 2 |
[U92(x1, x2, x3)] | = | 2 |
[a__U92(x1, x2, x3)] | = | 2 |
[U93(x1, x2, x3)] | = | 1 |
[a__U93(x1, x2, x3)] | = | 1 |
[U94(x1, x2)] | = | 1 |
[a__U94(x1, x2)] | = | 1 |
[a__length(x1)] | = | 2 |
[cons(x1, x2)] | = | 2 · x2 |
[nil] | = | 2 |
a__U93#(tt,L,N) | → | a__U94#(a__isNatKind(N),L) | (162) |
a__length#(cons(N,L)) | → | a__U91#(a__isNatList(L),L,N) | (182) |
The dependency pairs are split into 0 components.
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (142) |
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (145) |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (172) |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (136) |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (138) |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (140) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNatIListKind(nil) | → | tt | (37) |
a__isNatIListKind(zeros) | → | tt | (38) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (39) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (91) |
a__isNatKind(0) | → | tt | (40) |
a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | (41) |
a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) | (42) |
a__isNatKind(X) | → | isNatKind(X) | (96) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (17) |
a__U51(X1,X2) | → | U51(X1,X2) | (109) |
a__U52(tt) | → | tt | (18) |
a__U52(X) | → | U52(X) | (110) |
a__U71(tt) | → | tt | (20) |
a__U71(X) | → | U71(X) | (112) |
a__U61(tt) | → | tt | (19) |
a__U61(X) | → | U61(X) | (111) |
a__isNat(0) | → | tt | (31) |
a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1),V1) | (32) |
a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1),V1) | (33) |
a__isNat(X) | → | isNat(X) | (98) |
a__U21(tt,V1) | → | a__U22(a__isNatKind(V1),V1) | (5) |
a__U21(X1,X2) | → | U21(X1,X2) | (94) |
a__U22(tt,V1) | → | a__U23(a__isNat(V1)) | (6) |
a__U22(X1,X2) | → | U22(X1,X2) | (95) |
a__U23(tt) | → | tt | (7) |
a__U23(X) | → | U23(X) | (97) |
a__U11(tt,V1) | → | a__U12(a__isNatIListKind(V1),V1) | (2) |
a__U11(X1,X2) | → | U11(X1,X2) | (89) |
a__U12(tt,V1) | → | a__U13(a__isNatList(V1)) | (3) |
a__U12(X1,X2) | → | U12(X1,X2) | (90) |
a__isNatList(nil) | → | tt | (43) |
a__isNatList(cons(V1,V2)) | → | a__U81(a__isNatKind(V1),V1,V2) | (44) |
a__isNatList(X) | → | isNatList(X) | (93) |
a__U13(tt) | → | tt | (4) |
a__U13(X) | → | U13(X) | (92) |
a__U81(tt,V1,V2) | → | a__U82(a__isNatKind(V1),V1,V2) | (21) |
a__U81(X1,X2,X3) | → | U81(X1,X2,X3) | (113) |
a__U82(tt,V1,V2) | → | a__U83(a__isNatIListKind(V2),V1,V2) | (22) |
a__U82(X1,X2,X3) | → | U82(X1,X2,X3) | (114) |
a__U83(tt,V1,V2) | → | a__U84(a__isNatIListKind(V2),V1,V2) | (23) |
a__U83(X1,X2,X3) | → | U83(X1,X2,X3) | (115) |
a__U84(tt,V1,V2) | → | a__U85(a__isNat(V1),V2) | (24) |
a__U84(X1,X2,X3) | → | U84(X1,X2,X3) | (116) |
a__U85(tt,V2) | → | a__U86(a__isNatList(V2)) | (25) |
a__U85(X1,X2) | → | U85(X1,X2) | (117) |
a__U86(tt) | → | tt | (26) |
a__U86(X) | → | U86(X) | (118) |
We restrict the innermost strategy to the following left hand sides.
a__U11(x0,x1) |
a__U12(x0,x1) |
a__isNatIListKind(x0) |
a__U13(x0) |
a__isNatList(x0) |
a__U21(x0,x1) |
a__U22(x0,x1) |
a__isNatKind(x0) |
a__U23(x0) |
a__isNat(x0) |
a__U51(x0,x1) |
a__U52(x0) |
a__U61(x0) |
a__U71(x0) |
a__U81(x0,x1,x2) |
a__U82(x0,x1,x2) |
a__U83(x0,x1,x2) |
a__U84(x0,x1,x2) |
a__U85(x0,x1) |
a__U86(x0) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
a__U45#(tt,V2) | → | a__isNatIList#(V2) | (145) |
2 | ≥ | 1 | |
a__U43#(tt,V1,V2) | → | a__U44#(a__isNatIListKind(V2),V1,V2) | (140) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__isNatIList#(cons(V1,V2)) | → | a__U41#(a__isNatKind(V1),V1,V2) | (172) |
1 | > | 2 | |
1 | > | 3 | |
a__U44#(tt,V1,V2) | → | a__U45#(a__isNat(V1),V2) | (142) |
3 | ≥ | 2 | |
a__U41#(tt,V1,V2) | → | a__U42#(a__isNatKind(V1),V1,V2) | (136) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U42#(tt,V1,V2) | → | a__U43#(a__isNatIListKind(V2),V1,V2) | (138) |
2 | ≥ | 2 | |
3 | ≥ | 3 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U12#(tt,V1) | → | a__isNatList#(V1) | (127) |
a__isNatList#(cons(V1,V2)) | → | a__U81#(a__isNatKind(V1),V1,V2) | (180) |
a__U81#(tt,V1,V2) | → | a__U82#(a__isNatKind(V1),V1,V2) | (148) |
a__U82#(tt,V1,V2) | → | a__U83#(a__isNatIListKind(V2),V1,V2) | (150) |
a__U83#(tt,V1,V2) | → | a__U84#(a__isNatIListKind(V2),V1,V2) | (152) |
a__U84#(tt,V1,V2) | → | a__U85#(a__isNat(V1),V2) | (154) |
a__U85#(tt,V2) | → | a__isNatList#(V2) | (157) |
a__U84#(tt,V1,V2) | → | a__isNat#(V1) | (155) |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (166) |
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (124) |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (168) |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (128) |
a__U22#(tt,V1) | → | a__isNat#(V1) | (131) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNatKind(0) | → | tt | (40) |
a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | (41) |
a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) | (42) |
a__isNatKind(X) | → | isNatKind(X) | (96) |
a__U71(tt) | → | tt | (20) |
a__U71(X) | → | U71(X) | (112) |
a__isNatIListKind(nil) | → | tt | (37) |
a__isNatIListKind(zeros) | → | tt | (38) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (39) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (91) |
a__U61(tt) | → | tt | (19) |
a__U61(X) | → | U61(X) | (111) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (17) |
a__U51(X1,X2) | → | U51(X1,X2) | (109) |
a__U52(tt) | → | tt | (18) |
a__U52(X) | → | U52(X) | (110) |
a__isNat(0) | → | tt | (31) |
a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1),V1) | (32) |
a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1),V1) | (33) |
a__isNat(X) | → | isNat(X) | (98) |
a__U21(tt,V1) | → | a__U22(a__isNatKind(V1),V1) | (5) |
a__U21(X1,X2) | → | U21(X1,X2) | (94) |
a__U22(tt,V1) | → | a__U23(a__isNat(V1)) | (6) |
a__U22(X1,X2) | → | U22(X1,X2) | (95) |
a__U23(tt) | → | tt | (7) |
a__U23(X) | → | U23(X) | (97) |
a__U11(tt,V1) | → | a__U12(a__isNatIListKind(V1),V1) | (2) |
a__U11(X1,X2) | → | U11(X1,X2) | (89) |
a__U12(tt,V1) | → | a__U13(a__isNatList(V1)) | (3) |
a__U12(X1,X2) | → | U12(X1,X2) | (90) |
a__isNatList(nil) | → | tt | (43) |
a__isNatList(cons(V1,V2)) | → | a__U81(a__isNatKind(V1),V1,V2) | (44) |
a__isNatList(X) | → | isNatList(X) | (93) |
a__U13(tt) | → | tt | (4) |
a__U13(X) | → | U13(X) | (92) |
a__U81(tt,V1,V2) | → | a__U82(a__isNatKind(V1),V1,V2) | (21) |
a__U81(X1,X2,X3) | → | U81(X1,X2,X3) | (113) |
a__U82(tt,V1,V2) | → | a__U83(a__isNatIListKind(V2),V1,V2) | (22) |
a__U82(X1,X2,X3) | → | U82(X1,X2,X3) | (114) |
a__U83(tt,V1,V2) | → | a__U84(a__isNatIListKind(V2),V1,V2) | (23) |
a__U83(X1,X2,X3) | → | U83(X1,X2,X3) | (115) |
a__U84(tt,V1,V2) | → | a__U85(a__isNat(V1),V2) | (24) |
a__U84(X1,X2,X3) | → | U84(X1,X2,X3) | (116) |
a__U85(tt,V2) | → | a__U86(a__isNatList(V2)) | (25) |
a__U85(X1,X2) | → | U85(X1,X2) | (117) |
a__U86(tt) | → | tt | (26) |
a__U86(X) | → | U86(X) | (118) |
We restrict the innermost strategy to the following left hand sides.
a__U11(x0,x1) |
a__U12(x0,x1) |
a__isNatIListKind(x0) |
a__U13(x0) |
a__isNatList(x0) |
a__U21(x0,x1) |
a__U22(x0,x1) |
a__isNatKind(x0) |
a__U23(x0) |
a__isNat(x0) |
a__U51(x0,x1) |
a__U52(x0) |
a__U61(x0) |
a__U71(x0) |
a__U81(x0,x1,x2) |
a__U82(x0,x1,x2) |
a__U83(x0,x1,x2) |
a__U84(x0,x1,x2) |
a__U85(x0,x1) |
a__U86(x0) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
a__isNatList#(cons(V1,V2)) | → | a__U81#(a__isNatKind(V1),V1,V2) | (180) |
1 | > | 2 | |
1 | > | 3 | |
a__U11#(tt,V1) | → | a__U12#(a__isNatIListKind(V1),V1) | (124) |
2 | ≥ | 2 | |
a__U81#(tt,V1,V2) | → | a__U82#(a__isNatKind(V1),V1,V2) | (148) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U82#(tt,V1,V2) | → | a__U83#(a__isNatIListKind(V2),V1,V2) | (150) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U83#(tt,V1,V2) | → | a__U84#(a__isNatIListKind(V2),V1,V2) | (152) |
2 | ≥ | 2 | |
3 | ≥ | 3 | |
a__U85#(tt,V2) | → | a__isNatList#(V2) | (157) |
2 | ≥ | 1 | |
a__U12#(tt,V1) | → | a__isNatList#(V1) | (127) |
2 | ≥ | 1 | |
a__U84#(tt,V1,V2) | → | a__U85#(a__isNat(V1),V2) | (154) |
3 | ≥ | 2 | |
a__U84#(tt,V1,V2) | → | a__isNat#(V1) | (155) |
2 | ≥ | 1 | |
a__U22#(tt,V1) | → | a__isNat#(V1) | (131) |
2 | ≥ | 1 | |
a__U21#(tt,V1) | → | a__U22#(a__isNatKind(V1),V1) | (128) |
2 | ≥ | 2 | |
a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1),V1) | (166) |
1 | > | 2 | |
a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1),V1) | (168) |
1 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
a__U51#(tt,V2) | → | a__isNatIListKind#(V2) | (147) |
a__isNatIListKind#(cons(V1,V2)) | → | a__U51#(a__isNatKind(V1),V2) | (174) |
a__isNatIListKind#(cons(V1,V2)) | → | a__isNatKind#(V1) | (175) |
a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | (177) |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (179) |
We restrict the rewrite rules to the following usable rules of the DP problem.
a__isNatKind(0) | → | tt | (40) |
a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | (41) |
a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) | (42) |
a__isNatKind(X) | → | isNatKind(X) | (96) |
a__U71(tt) | → | tt | (20) |
a__U71(X) | → | U71(X) | (112) |
a__isNatIListKind(nil) | → | tt | (37) |
a__isNatIListKind(zeros) | → | tt | (38) |
a__isNatIListKind(cons(V1,V2)) | → | a__U51(a__isNatKind(V1),V2) | (39) |
a__isNatIListKind(X) | → | isNatIListKind(X) | (91) |
a__U61(tt) | → | tt | (19) |
a__U61(X) | → | U61(X) | (111) |
a__U51(tt,V2) | → | a__U52(a__isNatIListKind(V2)) | (17) |
a__U51(X1,X2) | → | U51(X1,X2) | (109) |
a__U52(tt) | → | tt | (18) |
a__U52(X) | → | U52(X) | (110) |
We restrict the innermost strategy to the following left hand sides.
a__isNatIListKind(x0) |
a__isNatKind(x0) |
a__U51(x0,x1) |
a__U52(x0) |
a__U61(x0) |
a__U71(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) | (174) |
1 | > | 2 | |
a__isNatIListKind#(cons(V1,V2)) | → | a__isNatKind#(V1) | (175) |
1 | > | 1 | |
a__U51#(tt,V2) | → | a__isNatIListKind#(V2) | (147) |
2 | ≥ | 1 | |
a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | (177) |
1 | > | 1 | |
a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | (179) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.