The TRS could not be proven terminating. The proof attempt took 60002 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].
| a__U91#(tt, V1, V2) | → | a__U92#(a__isNatKind(V1), V1, V2) | mark#(U62(X)) | → | a__U62#(mark(X)) | |
| mark#(U92(X1, X2, X3)) | → | a__U92#(mark(X1), X2, X3) | mark#(U46(X)) | → | a__U46#(mark(X)) | |
| mark#(U23(X)) | → | a__U23#(mark(X)) | a__U41#(tt, V1, V2) | → | a__U42#(a__isNatKind(V1), V1, V2) | |
| mark#(s(X)) | → | mark#(X) | mark#(U121(X1, X2)) | → | a__U121#(mark(X1), X2) | |
| mark#(U12(X1, X2)) | → | mark#(X1) | a__U12#(tt, V1) | → | a__U13#(a__isNatList(V1)) | |
| a__U51#(tt, V2) | → | a__U52#(a__isNatIListKind(V2)) | a__U131#(tt, IL, M, N) | → | a__isNatIListKind#(IL) | |
| a__U22#(tt, V1) | → | a__isNat#(V1) | a__U43#(tt, V1, V2) | → | a__isNatIListKind#(V2) | |
| mark#(U93(X1, X2, X3)) | → | a__U93#(mark(X1), X2, X3) | a__U114#(tt, L) | → | a__length#(mark(L)) | |
| a__U31#(tt, V) | → | a__U32#(a__isNatIListKind(V), V) | mark#(U105(X1, X2)) | → | a__U105#(mark(X1), X2) | |
| mark#(U52(X)) | → | mark#(X) | mark#(U122(X)) | → | mark#(X) | |
| a__U136#(tt, IL, M, N) | → | mark#(N) | mark#(U41(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U93(X1, X2, X3)) | → | mark#(X1) | a__U133#(tt, IL, M, N) | → | a__U134#(a__isNatKind(M), IL, M, N) | |
| mark#(U112(X1, X2, X3)) | → | mark#(X1) | mark#(U45(X1, X2)) | → | mark#(X1) | |
| a__U41#(tt, V1, V2) | → | a__isNatKind#(V1) | a__isNat#(length(V1)) | → | a__isNatIListKind#(V1) | |
| mark#(U95(X1, X2)) | → | mark#(X1) | mark#(U43(X1, X2, X3)) | → | mark#(X1) | |
| a__isNatIListKind#(cons(V1, V2)) | → | a__isNatKind#(V1) | mark#(U41(X1, X2, X3)) | → | a__U41#(mark(X1), X2, X3) | |
| a__U133#(tt, IL, M, N) | → | a__isNatKind#(M) | mark#(length(X)) | → | a__length#(mark(X)) | |
| mark#(U22(X1, X2)) | → | mark#(X1) | a__U21#(tt, V1) | → | a__isNatKind#(V1) | |
| a__U91#(tt, V1, V2) | → | a__isNatKind#(V1) | a__isNatList#(take(V1, V2)) | → | a__U101#(a__isNatKind(V1), V1, V2) | |
| a__isNatKind#(s(V1)) | → | a__U81#(a__isNatKind(V1)) | mark#(U113(X1, X2, X3)) | → | mark#(X1) | |
| a__length#(cons(N, L)) | → | a__isNatList#(L) | a__U32#(tt, V) | → | a__U33#(a__isNatList(V)) | |
| mark#(U45(X1, X2)) | → | a__U45#(mark(X1), X2) | a__U135#(tt, IL, M, N) | → | a__U136#(a__isNatKind(N), IL, M, N) | |
| a__U134#(tt, IL, M, N) | → | a__isNat#(N) | mark#(U51(X1, X2)) | → | a__U51#(mark(X1), X2) | |
| mark#(U92(X1, X2, X3)) | → | mark#(X1) | a__U104#(tt, V1, V2) | → | a__U105#(a__isNat(V1), V2) | |
| a__U95#(tt, V2) | → | a__isNatList#(V2) | a__U101#(tt, V1, V2) | → | a__U102#(a__isNatKind(V1), V1, V2) | |
| mark#(U122(X)) | → | a__U122#(mark(X)) | mark#(U133(X1, X2, X3, X4)) | → | a__U133#(mark(X1), X2, X3, X4) | |
| a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1), V1) | mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | |
| a__U135#(tt, IL, M, N) | → | a__isNatKind#(N) | mark#(U44(X1, X2, X3)) | → | a__U44#(mark(X1), X2, X3) | |
| a__U32#(tt, V) | → | a__isNatList#(V) | a__U45#(tt, V2) | → | a__isNatIList#(V2) | |
| mark#(take(X1, X2)) | → | mark#(X1) | a__U113#(tt, L, N) | → | a__isNatKind#(N) | |
| mark#(U134(X1, X2, X3, X4)) | → | mark#(X1) | mark#(U131(X1, X2, X3, X4)) | → | a__U131#(mark(X1), X2, X3, X4) | |
| mark#(U111(X1, X2, X3)) | → | a__U111#(mark(X1), X2, X3) | mark#(U32(X1, X2)) | → | a__U32#(mark(X1), X2) | |
| a__take#(0, IL) | → | a__isNatIList#(IL) | a__U113#(tt, L, N) | → | a__U114#(a__isNatKind(N), L) | |
| a__isNatList#(cons(V1, V2)) | → | a__isNatKind#(V1) | a__U134#(tt, IL, M, N) | → | a__U135#(a__isNat(N), IL, M, N) | |
| mark#(U33(X)) | → | a__U33#(mark(X)) | a__U131#(tt, IL, M, N) | → | a__U132#(a__isNatIListKind(IL), IL, M, N) | |
| a__isNat#(s(V1)) | → | a__isNatKind#(V1) | mark#(isNatList(X)) | → | a__isNatList#(X) | |
| mark#(U114(X1, X2)) | → | a__U114#(mark(X1), X2) | mark#(U104(X1, X2, X3)) | → | a__U104#(mark(X1), X2, X3) | |
| mark#(U12(X1, X2)) | → | a__U12#(mark(X1), X2) | mark#(U121(X1, X2)) | → | mark#(X1) | |
| mark#(U132(X1, X2, X3, X4)) | → | a__U132#(mark(X1), X2, X3, X4) | mark#(U135(X1, X2, X3, X4)) | → | a__U135#(mark(X1), X2, X3, X4) | |
| mark#(U42(X1, X2, X3)) | → | a__U42#(mark(X1), X2, X3) | mark#(U103(X1, X2, X3)) | → | a__U103#(mark(X1), X2, X3) | |
| mark#(U46(X)) | → | mark#(X) | mark#(U113(X1, X2, X3)) | → | a__U113#(mark(X1), X2, X3) | |
| mark#(U61(X1, X2)) | → | mark#(X1) | a__U111#(tt, L, N) | → | a__U112#(a__isNatIListKind(L), L, N) | |
| mark#(U21(X1, X2)) | → | mark#(X1) | mark#(U135(X1, X2, X3, X4)) | → | mark#(X1) | |
| a__U92#(tt, V1, V2) | → | a__isNatIListKind#(V2) | a__isNatKind#(length(V1)) | → | a__U71#(a__isNatIListKind(V1)) | |
| mark#(U102(X1, X2, X3)) | → | mark#(X1) | a__isNatIList#(cons(V1, V2)) | → | a__isNatKind#(V1) | |
| a__isNatList#(cons(V1, V2)) | → | a__U91#(a__isNatKind(V1), V1, V2) | a__U44#(tt, V1, V2) | → | a__isNat#(V1) | |
| a__U42#(tt, V1, V2) | → | a__U43#(a__isNatIListKind(V2), V1, V2) | a__isNatIListKind#(take(V1, V2)) | → | a__U61#(a__isNatKind(V1), V2) | |
| a__length#(cons(N, L)) | → | a__U111#(a__isNatList(L), L, N) | mark#(U91(X1, X2, X3)) | → | a__U91#(mark(X1), X2, X3) | |
| mark#(isNatKind(X)) | → | a__isNatKind#(X) | mark#(U13(X)) | → | mark#(X) | |
| mark#(U101(X1, X2, X3)) | → | mark#(X1) | mark#(U11(X1, X2)) | → | mark#(X1) | |
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | a__U94#(tt, V1, V2) | → | a__U95#(a__isNat(V1), V2) | |
| mark#(U13(X)) | → | a__U13#(mark(X)) | a__isNatList#(take(V1, V2)) | → | a__isNatKind#(V1) | |
| mark#(U94(X1, X2, X3)) | → | mark#(X1) | mark#(U136(X1, X2, X3, X4)) | → | mark#(X1) | |
| a__U44#(tt, V1, V2) | → | a__U45#(a__isNat(V1), V2) | a__U114#(tt, L) | → | mark#(L) | |
| a__U102#(tt, V1, V2) | → | a__U103#(a__isNatIListKind(V2), V1, V2) | a__isNatIList#(V) | → | a__U31#(a__isNatIListKind(V), V) | |
| mark#(cons(X1, X2)) | → | mark#(X1) | mark#(U42(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U101(X1, X2, X3)) | → | a__U101#(mark(X1), X2, X3) | a__U104#(tt, V1, V2) | → | a__isNat#(V1) | |
| mark#(U62(X)) | → | mark#(X) | mark#(U32(X1, X2)) | → | mark#(X1) | |
| a__U132#(tt, IL, M, N) | → | a__isNat#(M) | mark#(U106(X)) | → | a__U106#(mark(X)) | |
| mark#(isNat(X)) | → | a__isNat#(X) | mark#(U91(X1, X2, X3)) | → | mark#(X1) | |
| mark#(zeros) | → | a__zeros# | mark#(U96(X)) | → | mark#(X) | |
| mark#(U33(X)) | → | mark#(X) | a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | |
| a__take#(s(M), cons(N, IL)) | → | a__isNatIList#(IL) | a__U11#(tt, V1) | → | a__isNatIListKind#(V1) | |
| a__U51#(tt, V2) | → | a__isNatIListKind#(V2) | mark#(U23(X)) | → | mark#(X) | |
| mark#(U102(X1, X2, X3)) | → | a__U102#(mark(X1), X2, X3) | mark#(length(X)) | → | mark#(X) | |
| a__U93#(tt, V1, V2) | → | a__U94#(a__isNatIListKind(V2), V1, V2) | a__U12#(tt, V1) | → | a__isNatList#(V1) | |
| a__U61#(tt, V2) | → | a__isNatIListKind#(V2) | mark#(U95(X1, X2)) | → | a__U95#(mark(X1), X2) | |
| mark#(U131(X1, X2, X3, X4)) | → | mark#(X1) | a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1), V1) | |
| mark#(U105(X1, X2)) | → | mark#(X1) | a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNatKind(V1), V1, V2) | |
| a__U111#(tt, L, N) | → | a__isNatIListKind#(L) | mark#(U133(X1, X2, X3, X4)) | → | mark#(X1) | |
| a__U112#(tt, L, N) | → | a__U113#(a__isNat(N), L, N) | a__U121#(tt, IL) | → | a__isNatIListKind#(IL) | |
| mark#(U52(X)) | → | a__U52#(mark(X)) | mark#(U71(X)) | → | a__U71#(mark(X)) | |
| mark#(U71(X)) | → | mark#(X) | mark#(isNatIListKind(X)) | → | a__isNatIListKind#(X) | |
| a__U132#(tt, IL, M, N) | → | a__U133#(a__isNat(M), IL, M, N) | a__U103#(tt, V1, V2) | → | a__isNatIListKind#(V2) | |
| mark#(U103(X1, X2, X3)) | → | mark#(X1) | mark#(U104(X1, X2, X3)) | → | mark#(X1) | |
| a__U121#(tt, IL) | → | a__U122#(a__isNatIListKind(IL)) | mark#(U22(X1, X2)) | → | a__U22#(mark(X1), X2) | |
| a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) | a__U102#(tt, V1, V2) | → | a__isNatIListKind#(V2) | |
| mark#(U134(X1, X2, X3, X4)) | → | a__U134#(mark(X1), X2, X3, X4) | a__U112#(tt, L, N) | → | a__isNat#(N) | |
| mark#(U81(X)) | → | mark#(X) | mark#(U31(X1, X2)) | → | mark#(X1) | |
| mark#(U112(X1, X2, X3)) | → | a__U112#(mark(X1), X2, X3) | a__U61#(tt, V2) | → | a__U62#(a__isNatIListKind(V2)) | |
| a__U22#(tt, V1) | → | a__U23#(a__isNat(V1)) | mark#(U106(X)) | → | mark#(X) | |
| a__isNatIListKind#(take(V1, V2)) | → | a__isNatKind#(V1) | mark#(U136(X1, X2, X3, X4)) | → | a__U136#(mark(X1), X2, X3, X4) | |
| mark#(U96(X)) | → | a__U96#(mark(X)) | a__U11#(tt, V1) | → | a__U12#(a__isNatIListKind(V1), V1) | |
| mark#(U61(X1, X2)) | → | a__U61#(mark(X1), X2) | a__U42#(tt, V1, V2) | → | a__isNatIListKind#(V2) | |
| mark#(U114(X1, X2)) | → | mark#(X1) | a__U105#(tt, V2) | → | a__isNatIList#(V2) | |
| a__U21#(tt, V1) | → | a__U22#(a__isNatKind(V1), V1) | a__take#(s(M), cons(N, IL)) | → | a__U131#(a__isNatIList(IL), IL, M, N) | |
| a__U103#(tt, V1, V2) | → | a__U104#(a__isNatIListKind(V2), V1, V2) | a__U43#(tt, V1, V2) | → | a__U44#(a__isNatIListKind(V2), V1, V2) | |
| a__isNatIList#(V) | → | a__isNatIListKind#(V) | a__U101#(tt, V1, V2) | → | a__isNatKind#(V1) | |
| mark#(U31(X1, X2)) | → | a__U31#(mark(X1), X2) | mark#(U51(X1, X2)) | → | mark#(X1) | |
| mark#(U44(X1, X2, X3)) | → | mark#(X1) | a__take#(0, IL) | → | a__U121#(a__isNatIList(IL), IL) | |
| mark#(U94(X1, X2, X3)) | → | a__U94#(mark(X1), X2, X3) | mark#(U111(X1, X2, X3)) | → | mark#(X1) | |
| a__isNatIListKind#(cons(V1, V2)) | → | a__U51#(a__isNatKind(V1), V2) | a__U45#(tt, V2) | → | a__U46#(a__isNatIList(V2)) | |
| a__U31#(tt, V) | → | a__isNatIListKind#(V) | a__U93#(tt, V1, V2) | → | a__isNatIListKind#(V2) | |
| a__U95#(tt, V2) | → | a__U96#(a__isNatList(V2)) | a__U92#(tt, V1, V2) | → | a__U93#(a__isNatIListKind(V2), V1, V2) | |
| mark#(U21(X1, X2)) | → | a__U21#(mark(X1), X2) | mark#(U132(X1, X2, X3, X4)) | → | mark#(X1) | |
| mark#(U43(X1, X2, X3)) | → | a__U43#(mark(X1), X2, X3) | a__U105#(tt, V2) | → | a__U106#(a__isNatIList(V2)) | |
| mark#(U11(X1, X2)) | → | a__U11#(mark(X1), X2) | mark#(take(X1, X2)) | → | mark#(X2) | |
| mark#(U81(X)) | → | a__U81#(mark(X)) | a__U94#(tt, V1, V2) | → | a__isNat#(V1) |
| a__zeros | → | cons(0, zeros) | a__U101(tt, V1, V2) | → | a__U102(a__isNatKind(V1), V1, V2) | |
| a__U102(tt, V1, V2) | → | a__U103(a__isNatIListKind(V2), V1, V2) | a__U103(tt, V1, V2) | → | a__U104(a__isNatIListKind(V2), V1, V2) | |
| a__U104(tt, V1, V2) | → | a__U105(a__isNat(V1), V2) | a__U105(tt, V2) | → | a__U106(a__isNatIList(V2)) | |
| a__U106(tt) | → | tt | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) | |
| a__U111(tt, L, N) | → | a__U112(a__isNatIListKind(L), L, N) | a__U112(tt, L, N) | → | a__U113(a__isNat(N), L, N) | |
| a__U113(tt, L, N) | → | a__U114(a__isNatKind(N), L) | a__U114(tt, L) | → | s(a__length(mark(L))) | |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | a__U121(tt, IL) | → | a__U122(a__isNatIListKind(IL)) | |
| a__U122(tt) | → | nil | a__U13(tt) | → | tt | |
| a__U131(tt, IL, M, N) | → | a__U132(a__isNatIListKind(IL), IL, M, N) | a__U132(tt, IL, M, N) | → | a__U133(a__isNat(M), IL, M, N) | |
| a__U133(tt, IL, M, N) | → | a__U134(a__isNatKind(M), IL, M, N) | a__U134(tt, IL, M, N) | → | a__U135(a__isNat(N), IL, M, N) | |
| a__U135(tt, IL, M, N) | → | a__U136(a__isNatKind(N), IL, M, N) | a__U136(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) | |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) | |
| a__U23(tt) | → | tt | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) | |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | a__U33(tt) | → | tt | |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) | |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) | |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | a__U46(tt) | → | tt | |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | a__U52(tt) | → | tt | |
| a__U61(tt, V2) | → | a__U62(a__isNatIListKind(V2)) | a__U62(tt) | → | tt | |
| a__U71(tt) | → | tt | a__U81(tt) | → | tt | |
| a__U91(tt, V1, V2) | → | a__U92(a__isNatKind(V1), V1, V2) | a__U92(tt, V1, V2) | → | a__U93(a__isNatIListKind(V2), V1, V2) | |
| a__U93(tt, V1, V2) | → | a__U94(a__isNatIListKind(V2), V1, V2) | a__U94(tt, V1, V2) | → | a__U95(a__isNat(V1), V2) | |
| a__U95(tt, V2) | → | a__U96(a__isNatList(V2)) | a__U96(tt) | → | tt | |
| a__isNat(0) | → | tt | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) | |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) | |
| a__isNatIList(zeros) | → | tt | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) | |
| a__isNatIListKind(nil) | → | tt | a__isNatIListKind(zeros) | → | tt | |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | a__isNatIListKind(take(V1, V2)) | → | a__U61(a__isNatKind(V1), V2) | |
| a__isNatKind(0) | → | tt | a__isNatKind(length(V1)) | → | a__U71(a__isNatIListKind(V1)) | |
| a__isNatKind(s(V1)) | → | a__U81(a__isNatKind(V1)) | a__isNatList(nil) | → | tt | |
| a__isNatList(cons(V1, V2)) | → | a__U91(a__isNatKind(V1), V1, V2) | a__isNatList(take(V1, V2)) | → | a__U101(a__isNatKind(V1), V1, V2) | |
| a__length(nil) | → | 0 | a__length(cons(N, L)) | → | a__U111(a__isNatList(L), L, N) | |
| a__take(0, IL) | → | a__U121(a__isNatIList(IL), IL) | a__take(s(M), cons(N, IL)) | → | a__U131(a__isNatIList(IL), IL, M, N) | |
| mark(zeros) | → | a__zeros | mark(U101(X1, X2, X3)) | → | a__U101(mark(X1), X2, X3) | |
| mark(U102(X1, X2, X3)) | → | a__U102(mark(X1), X2, X3) | mark(isNatKind(X)) | → | a__isNatKind(X) | |
| mark(U103(X1, X2, X3)) | → | a__U103(mark(X1), X2, X3) | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) | |
| mark(U104(X1, X2, X3)) | → | a__U104(mark(X1), X2, X3) | mark(U105(X1, X2)) | → | a__U105(mark(X1), X2) | |
| mark(isNat(X)) | → | a__isNat(X) | mark(U106(X)) | → | a__U106(mark(X)) | |
| mark(isNatIList(X)) | → | a__isNatIList(X) | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | mark(U111(X1, X2, X3)) | → | a__U111(mark(X1), X2, X3) | |
| mark(U112(X1, X2, X3)) | → | a__U112(mark(X1), X2, X3) | mark(U113(X1, X2, X3)) | → | a__U113(mark(X1), X2, X3) | |
| mark(U114(X1, X2)) | → | a__U114(mark(X1), X2) | mark(length(X)) | → | a__length(mark(X)) | |
| mark(U13(X)) | → | a__U13(mark(X)) | mark(isNatList(X)) | → | a__isNatList(X) | |
| mark(U121(X1, X2)) | → | a__U121(mark(X1), X2) | mark(U122(X)) | → | a__U122(mark(X)) | |
| mark(U131(X1, X2, X3, X4)) | → | a__U131(mark(X1), X2, X3, X4) | mark(U132(X1, X2, X3, X4)) | → | a__U132(mark(X1), X2, X3, X4) | |
| mark(U133(X1, X2, X3, X4)) | → | a__U133(mark(X1), X2, X3, X4) | mark(U134(X1, X2, X3, X4)) | → | a__U134(mark(X1), X2, X3, X4) | |
| mark(U135(X1, X2, X3, X4)) | → | a__U135(mark(X1), X2, X3, X4) | mark(U136(X1, X2, X3, X4)) | → | a__U136(mark(X1), X2, X3, X4) | |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | |
| mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) | mark(U23(X)) | → | a__U23(mark(X)) | |
| mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) | mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | |
| mark(U33(X)) | → | a__U33(mark(X)) | mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | |
| mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) | mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | |
| mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) | mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | |
| mark(U46(X)) | → | a__U46(mark(X)) | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) | |
| mark(U52(X)) | → | a__U52(mark(X)) | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) | |
| mark(U62(X)) | → | a__U62(mark(X)) | mark(U71(X)) | → | a__U71(mark(X)) | |
| mark(U81(X)) | → | a__U81(mark(X)) | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) | |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) | |
| mark(U94(X1, X2, X3)) | → | a__U94(mark(X1), X2, X3) | mark(U95(X1, X2)) | → | a__U95(mark(X1), X2) | |
| mark(U96(X)) | → | a__U96(mark(X)) | mark(cons(X1, X2)) | → | cons(mark(X1), X2) | |
| mark(0) | → | 0 | mark(tt) | → | tt | |
| mark(s(X)) | → | s(mark(X)) | mark(nil) | → | nil | |
| a__zeros | → | zeros | a__U101(X1, X2, X3) | → | U101(X1, X2, X3) | |
| a__U102(X1, X2, X3) | → | U102(X1, X2, X3) | a__isNatKind(X) | → | isNatKind(X) | |
| a__U103(X1, X2, X3) | → | U103(X1, X2, X3) | a__isNatIListKind(X) | → | isNatIListKind(X) | |
| a__U104(X1, X2, X3) | → | U104(X1, X2, X3) | a__U105(X1, X2) | → | U105(X1, X2) | |
| a__isNat(X) | → | isNat(X) | a__U106(X) | → | U106(X) | |
| a__isNatIList(X) | → | isNatIList(X) | a__U11(X1, X2) | → | U11(X1, X2) | |
| a__U12(X1, X2) | → | U12(X1, X2) | a__U111(X1, X2, X3) | → | U111(X1, X2, X3) | |
| a__U112(X1, X2, X3) | → | U112(X1, X2, X3) | a__U113(X1, X2, X3) | → | U113(X1, X2, X3) | |
| a__U114(X1, X2) | → | U114(X1, X2) | a__length(X) | → | length(X) | |
| a__U13(X) | → | U13(X) | a__isNatList(X) | → | isNatList(X) | |
| a__U121(X1, X2) | → | U121(X1, X2) | a__U122(X) | → | U122(X) | |
| a__U131(X1, X2, X3, X4) | → | U131(X1, X2, X3, X4) | a__U132(X1, X2, X3, X4) | → | U132(X1, X2, X3, X4) | |
| a__U133(X1, X2, X3, X4) | → | U133(X1, X2, X3, X4) | a__U134(X1, X2, X3, X4) | → | U134(X1, X2, X3, X4) | |
| a__U135(X1, X2, X3, X4) | → | U135(X1, X2, X3, X4) | a__U136(X1, X2, X3, X4) | → | U136(X1, X2, X3, X4) | |
| a__take(X1, X2) | → | take(X1, X2) | a__U21(X1, X2) | → | U21(X1, X2) | |
| a__U22(X1, X2) | → | U22(X1, X2) | a__U23(X) | → | U23(X) | |
| a__U31(X1, X2) | → | U31(X1, X2) | a__U32(X1, X2) | → | U32(X1, X2) | |
| a__U33(X) | → | U33(X) | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) | |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) | |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | a__U45(X1, X2) | → | U45(X1, X2) | |
| a__U46(X) | → | U46(X) | a__U51(X1, X2) | → | U51(X1, X2) | |
| a__U52(X) | → | U52(X) | a__U61(X1, X2) | → | U61(X1, X2) | |
| a__U62(X) | → | U62(X) | a__U71(X) | → | U71(X) | |
| a__U81(X) | → | U81(X) | a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | |
| a__U92(X1, X2, X3) | → | U92(X1, X2, X3) | a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | |
| a__U94(X1, X2, X3) | → | U94(X1, X2, X3) | a__U95(X1, X2) | → | U95(X1, X2) | |
| a__U96(X) | → | U96(X) |
Termination of terms over the following signature is verified: a__U121, a__U122, U104, U105, U106, U112, U111, U62, U114, U61, U113, a__U41, a__U43, a__U42, a__U45, a__U44, a__U114, a__U46, a__U112, a__U113, a__U111, U71, 0, U122, U121, zeros, a__isNat, a__U32, a__U31, a__U106, a__U105, a__U104, a__U33, a__U103, a__take, isNatIListKind, a__U96, a__U95, a__isNatIListKind, U46, U45, a__isNatList, U44, U132, U131, U43, a__U91, U134, U42, a__U92, U133, U41, a__U93, U136, a__U94, U135, a__U23, length, a__U22, a__U136, a__U21, cons, a__U131, a__U134, a__U135, a__U132, a__U133, U51, s, isNatList, tt, U52, a__U13, a__U12, a__U11, a__isNatKind, a__U71, U23, U21, U22, isNatIList, isNatKind, mark, a__isNatIList, a__U81, U31, U32, U33, a__U51, a__U52, U96, U94, U95, isNat, U93, U92, U91, a__U102, a__U101, a__zeros, a__U62, a__length, take, U81, U11, U12, U13, a__U61, U102, U103, nil, U101