The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].
| a__isLNat#(cons(V1, V2)) | → | a__U51#(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | mark#(U62(X)) | → | a__U62#(mark(X)) | |
| a__isLNatKind#(afterNth(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | a__isLNat#(take(V1, V2)) | → | a__isNaturalKind#(V1) | |
| a__U21#(tt, X) | → | mark#(X) | a__U121#(tt, V1) | → | a__U122#(a__isNatural(V1)) | |
| a__isNatural#(sel(V1, V2)) | → | a__isNaturalKind#(V1) | a__U11#(tt, N, XS) | → | a__snd#(a__splitAt(mark(N), mark(XS))) | |
| a__isLNatKind#(natsFrom(V1)) | → | a__isNaturalKind#(V1) | mark#(s(X)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | mark#(X1) | mark#(U121(X1, X2)) | → | a__U121#(mark(X1), X2) | |
| mark#(U72(X)) | → | mark#(X) | mark#(U171(X1, X2, X3)) | → | mark#(X1) | |
| a__isLNat#(take(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | mark#(afterNth(X1, X2)) | → | mark#(X1) | |
| mark#(U122(X)) | → | mark#(X) | mark#(U92(X)) | → | a__U92#(mark(X)) | |
| a__U171#(tt, N, XS) | → | a__head#(a__afterNth(mark(N), mark(XS))) | a__isLNatKind#(snd(V1)) | → | a__isPLNatKind#(V1) | |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) | mark#(U41(X1, X2, X3)) | → | mark#(X1) | |
| a__take#(N, XS) | → | a__U221#(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | mark#(U111(X1, X2)) | → | mark#(X1) | |
| a__U41#(tt, V1, V2) | → | a__isNatural#(V1) | a__isLNatKind#(take(V1, V2)) | → | a__isNaturalKind#(V1) | |
| mark#(U11(X1, X2, X3)) | → | mark#(X1) | a__U181#(tt, Y) | → | mark#(Y) | |
| mark#(U153(X)) | → | a__U153#(mark(X)) | a__snd#(pair(X, Y)) | → | a__U181#(a__and(a__and(a__isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) | |
| a__U171#(tt, N, XS) | → | a__afterNth#(mark(N), mark(XS)) | mark#(U141(X1, X2, X3)) | → | mark#(X1) | |
| a__U31#(tt, N) | → | mark#(N) | mark#(U211(X1, X2)) | → | a__U211#(mark(X1), X2) | |
| a__isPLNatKind#(pair(V1, V2)) | → | a__isLNatKind#(V1) | mark#(U41(X1, X2, X3)) | → | a__U41#(mark(X1), X2, X3) | |
| mark#(U102(X1, X2)) | → | a__U102#(mark(X1), X2) | a__U11#(tt, N, XS) | → | mark#(XS) | |
| a__U151#(tt, V1, V2) | → | a__isNatural#(V1) | mark#(head(X)) | → | mark#(X) | |
| mark#(splitAt(X1, X2)) | → | mark#(X1) | mark#(isPLNat(X)) | → | a__isPLNat#(X) | |
| a__U42#(tt, V2) | → | a__U43#(a__isLNat(V2)) | mark#(isNatural(X)) | → | a__isNatural#(X) | |
| mark#(U141(X1, X2, X3)) | → | a__U141#(mark(X1), X2, X3) | a__isNaturalKind#(sel(V1, V2)) | → | a__isNaturalKind#(V1) | |
| mark#(fst(X)) | → | a__fst#(mark(X)) | a__U42#(tt, V2) | → | a__isLNat#(V2) | |
| a__U91#(tt, V1) | → | a__U92#(a__isLNat(V1)) | a__U221#(tt, N, XS) | → | mark#(N) | |
| mark#(U143(X)) | → | mark#(X) | mark#(fst(X)) | → | mark#(X) | |
| a__isLNat#(afterNth(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | mark#(U42(X1, X2)) | → | mark#(X1) | |
| mark#(U103(X)) | → | mark#(X) | mark#(U221(X1, X2, X3)) | → | mark#(X1) | |
| a__splitAt#(s(N), cons(X, XS)) | → | a__isNatural#(N) | mark#(snd(X)) | → | mark#(X) | |
| a__U71#(tt, V1) | → | a__U72#(a__isNatural(V1)) | mark#(natsFrom(X)) | → | mark#(X) | |
| a__U191#(tt, XS) | → | mark#(XS) | mark#(U201(X1, X2, X3, X4)) | → | mark#(X1) | |
| a__isNatural#(sel(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | mark#(U102(X1, X2)) | → | mark#(X1) | |
| a__splitAt#(s(N), cons(X, XS)) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | mark#(U122(X)) | → | a__U122#(mark(X)) | |
| a__splitAt#(s(N), cons(X, XS)) | → | a__U201#(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) | mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | |
| a__U151#(tt, V1, V2) | → | a__U152#(a__isNatural(V1), V2) | a__isPLNat#(pair(V1, V2)) | → | a__and#(a__isLNatKind(V1), isLNatKind(V2)) | |
| a__natsFrom#(N) | → | a__U161#(a__and(a__isNatural(N), isNaturalKind(N)), N) | mark#(splitAt(X1, X2)) | → | a__splitAt#(mark(X1), mark(X2)) | |
| mark#(U191(X1, X2)) | → | mark#(X1) | a__U201#(tt, N, X, XS) | → | mark#(N) | |
| a__U81#(tt, V1) | → | a__isPLNat#(V1) | mark#(take(X1, X2)) | → | mark#(X1) | |
| a__sel#(N, XS) | → | a__isNatural#(N) | mark#(isNaturalKind(X)) | → | a__isNaturalKind#(X) | |
| a__snd#(pair(X, Y)) | → | a__and#(a__isLNat(X), isLNatKind(X)) | a__sel#(N, XS) | → | a__U171#(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | |
| a__U61#(tt, V1) | → | a__U62#(a__isPLNat(V1)) | a__isLNat#(snd(V1)) | → | a__isPLNatKind#(V1) | |
| mark#(U91(X1, X2)) | → | a__U91#(mark(X1), X2) | a__U131#(tt, V1, V2) | → | a__isNatural#(V1) | |
| a__U11#(tt, N, XS) | → | a__splitAt#(mark(N), mark(XS)) | mark#(U53(X)) | → | a__U53#(mark(X)) | |
| mark#(U71(X1, X2)) | → | a__U71#(mark(X1), X2) | a__fst#(pair(X, Y)) | → | a__and#(a__and(a__isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) | |
| a__U111#(tt, V1) | → | a__isLNat#(V1) | a__fst#(pair(X, Y)) | → | a__isLNat#(X) | |
| a__U141#(tt, V1, V2) | → | a__U142#(a__isLNat(V1), V2) | mark#(U71(X1, X2)) | → | mark#(X1) | |
| a__U211#(tt, XS) | → | mark#(XS) | a__head#(cons(N, XS)) | → | a__and#(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | |
| mark#(U121(X1, X2)) | → | mark#(X1) | a__isLNat#(cons(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | |
| mark#(U133(X)) | → | mark#(X) | mark#(U142(X1, X2)) | → | a__U142#(mark(X1), X2) | |
| mark#(U211(X1, X2)) | → | mark#(X1) | a__U132#(tt, V2) | → | a__U133#(a__isLNat(V2)) | |
| mark#(U11(X1, X2, X3)) | → | a__U11#(mark(X1), X2, X3) | mark#(U61(X1, X2)) | → | mark#(X1) | |
| a__isLNat#(fst(V1)) | → | a__isPLNatKind#(V1) | a__afterNth#(N, XS) | → | a__U11#(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | |
| a__U152#(tt, V2) | → | a__U153#(a__isLNat(V2)) | a__U81#(tt, V1) | → | a__U82#(a__isPLNat(V1)) | |
| mark#(U181(X1, X2)) | → | mark#(X1) | mark#(U21(X1, X2)) | → | mark#(X1) | |
| mark#(U221(X1, X2, X3)) | → | a__U221#(mark(X1), X2, X3) | a__U71#(tt, V1) | → | a__isNatural#(V1) | |
| a__U171#(tt, N, XS) | → | mark#(XS) | mark#(sel(X1, X2)) | → | mark#(X2) | |
| mark#(tail(X)) | → | a__tail#(mark(X)) | a__isLNatKind#(cons(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | |
| a__U102#(tt, V2) | → | a__isLNat#(V2) | mark#(U151(X1, X2, X3)) | → | a__U151#(mark(X1), X2, X3) | |
| a__fst#(pair(X, Y)) | → | a__U21#(a__and(a__and(a__isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) | a__isPLNat#(splitAt(V1, V2)) | → | a__U151#(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | |
| mark#(U153(X)) | → | mark#(X) | mark#(splitAt(X1, X2)) | → | mark#(X2) | |
| a__isNatural#(sel(V1, V2)) | → | a__U131#(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | mark#(U82(X)) | → | a__U82#(mark(X)) | |
| a__isLNat#(tail(V1)) | → | a__U91#(a__isLNatKind(V1), V1) | mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | |
| mark#(U152(X1, X2)) | → | mark#(X1) | mark#(U103(X)) | → | a__U103#(mark(X)) | |
| mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | mark#(U101(X1, X2, X3)) | → | mark#(X1) | |
| a__isPLNat#(splitAt(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | mark#(pair(X1, X2)) | → | mark#(X2) | |
| a__U171#(tt, N, XS) | → | mark#(N) | a__isLNat#(tail(V1)) | → | a__isLNatKind#(V1) | |
| a__head#(cons(N, XS)) | → | a__U31#(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | a__and#(tt, X) | → | mark#(X) | |
| a__U52#(tt, V2) | → | a__U53#(a__isLNat(V2)) | a__isLNatKind#(tail(V1)) | → | a__isLNatKind#(V1) | |
| a__afterNth#(N, XS) | → | a__and#(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | a__isLNat#(snd(V1)) | → | a__U81#(a__isPLNatKind(V1), V1) | |
| mark#(U53(X)) | → | mark#(X) | a__snd#(pair(X, Y)) | → | a__isLNat#(X) | |
| a__isLNatKind#(take(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| a__isNaturalKind#(sel(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | a__U51#(tt, V1, V2) | → | a__isNatural#(V1) | |
| a__U121#(tt, V1) | → | a__isNatural#(V1) | a__splitAt#(0, XS) | → | a__isLNat#(XS) | |
| mark#(U101(X1, X2, X3)) | → | a__U101#(mark(X1), X2, X3) | a__isLNat#(cons(V1, V2)) | → | a__isNaturalKind#(V1) | |
| a__U202#(pair(YS, ZS), X) | → | mark#(ZS) | mark#(and(X1, X2)) | → | mark#(X1) | |
| a__U52#(tt, V2) | → | a__isLNat#(V2) | mark#(pair(X1, X2)) | → | mark#(X1) | |
| a__isNaturalKind#(head(V1)) | → | a__isLNatKind#(V1) | a__isLNat#(natsFrom(V1)) | → | a__U71#(a__isNaturalKind(V1), V1) | |
| mark#(tail(X)) | → | mark#(X) | mark#(U161(X1, X2)) | → | a__U161#(mark(X1), X2) | |
| mark#(U62(X)) | → | mark#(X) | a__splitAt#(s(N), cons(X, XS)) | → | a__and#(a__and(a__isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))) | |
| a__head#(cons(N, XS)) | → | a__isNatural#(N) | a__U111#(tt, V1) | → | a__U112#(a__isLNat(V1)) | |
| a__splitAt#(0, XS) | → | a__U191#(a__and(a__isLNat(XS), isLNatKind(XS)), XS) | mark#(afterNth(X1, X2)) | → | mark#(X2) | |
| a__isLNat#(take(V1, V2)) | → | a__U101#(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | a__take#(N, XS) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | |
| a__isNatural#(head(V1)) | → | a__isLNatKind#(V1) | a__isPLNat#(pair(V1, V2)) | → | a__U141#(a__and(a__isLNatKind(V1), isLNatKind(V2)), V1, V2) | |
| a__tail#(cons(N, XS)) | → | a__and#(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | mark#(U43(X)) | → | a__U43#(mark(X)) | |
| a__head#(cons(N, XS)) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | a__take#(N, XS) | → | a__and#(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | |
| mark#(U133(X)) | → | a__U133#(mark(X)) | mark#(U181(X1, X2)) | → | a__U181#(mark(X1), X2) | |
| mark#(U132(X1, X2)) | → | mark#(X1) | a__afterNth#(N, XS) | → | a__isNatural#(N) | |
| a__U221#(tt, N, XS) | → | a__fst#(a__splitAt(mark(N), mark(XS))) | mark#(U51(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U52(X1, X2)) | → | a__U52#(mark(X1), X2) | mark#(head(X)) | → | a__head#(mark(X)) | |
| a__U41#(tt, V1, V2) | → | a__U42#(a__isNatural(V1), V2) | a__sel#(N, XS) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | |
| a__splitAt#(0, XS) | → | a__and#(a__isLNat(XS), isLNatKind(XS)) | mark#(U143(X)) | → | a__U143#(mark(X)) | |
| a__tail#(cons(N, XS)) | → | a__isNatural#(N) | a__isPLNatKind#(pair(V1, V2)) | → | a__and#(a__isLNatKind(V1), isLNatKind(V2)) | |
| a__U101#(tt, V1, V2) | → | a__U102#(a__isNatural(V1), V2) | mark#(U131(X1, X2, X3)) | → | a__U131#(mark(X1), X2, X3) | |
| a__isPLNat#(splitAt(V1, V2)) | → | a__isNaturalKind#(V1) | mark#(U51(X1, X2, X3)) | → | a__U51#(mark(X1), X2, X3) | |
| mark#(U202(X1, X2)) | → | mark#(X1) | mark#(U43(X)) | → | mark#(X) | |
| a__U11#(tt, N, XS) | → | mark#(N) | a__snd#(pair(X, Y)) | → | a__and#(a__and(a__isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))) | |
| mark#(U131(X1, X2, X3)) | → | mark#(X1) | a__U61#(tt, V1) | → | a__isPLNat#(V1) | |
| a__U152#(tt, V2) | → | a__isLNat#(V2) | a__isPLNatKind#(splitAt(V1, V2)) | → | a__and#(a__isNaturalKind(V1), isLNatKind(V2)) | |
| mark#(afterNth(X1, X2)) | → | a__afterNth#(mark(X1), mark(X2)) | a__isNatural#(head(V1)) | → | a__U111#(a__isLNatKind(V1), V1) | |
| a__U201#(tt, N, X, XS) | → | a__U202#(a__splitAt(mark(N), mark(XS)), X) | a__isLNat#(afterNth(V1, V2)) | → | a__isNaturalKind#(V1) | |
| a__take#(N, XS) | → | a__isNatural#(N) | mark#(U72(X)) | → | a__U72#(mark(X)) | |
| a__isPLNat#(pair(V1, V2)) | → | a__isLNatKind#(V1) | a__isNaturalKind#(s(V1)) | → | a__isNaturalKind#(V1) | |
| a__U221#(tt, N, XS) | → | mark#(XS) | mark#(U191(X1, X2)) | → | a__U191#(mark(X1), X2) | |
| mark#(U112(X)) | → | a__U112#(mark(X)) | mark#(U31(X1, X2)) | → | mark#(X1) | |
| a__U142#(tt, V2) | → | a__isLNat#(V2) | mark#(U81(X1, X2)) | → | a__U81#(mark(X1), X2) | |
| mark#(U81(X1, X2)) | → | mark#(X1) | a__U51#(tt, V1, V2) | → | a__U52#(a__isNatural(V1), V2) | |
| mark#(U42(X1, X2)) | → | a__U42#(mark(X1), X2) | mark#(isLNat(X)) | → | a__isLNat#(X) | |
| mark#(U82(X)) | → | mark#(X) | mark#(U61(X1, X2)) | → | a__U61#(mark(X1), X2) | |
| a__U131#(tt, V1, V2) | → | a__U132#(a__isNatural(V1), V2) | a__U201#(tt, N, X, XS) | → | mark#(XS) | |
| a__U221#(tt, N, XS) | → | a__splitAt#(mark(N), mark(XS)) | mark#(U112(X)) | → | mark#(X) | |
| mark#(U161(X1, X2)) | → | mark#(X1) | a__afterNth#(N, XS) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | |
| mark#(snd(X)) | → | a__snd#(mark(X)) | a__U201#(tt, N, X, XS) | → | a__splitAt#(mark(N), mark(XS)) | |
| a__isLNatKind#(cons(V1, V2)) | → | a__isNaturalKind#(V1) | mark#(U91(X1, X2)) | → | mark#(X1) | |
| a__isLNatKind#(fst(V1)) | → | a__isPLNatKind#(V1) | mark#(U111(X1, X2)) | → | a__U111#(mark(X1), X2) | |
| mark#(U151(X1, X2, X3)) | → | mark#(X1) | a__U202#(pair(YS, ZS), X) | → | mark#(X) | |
| mark#(U152(X1, X2)) | → | a__U152#(mark(X1), X2) | mark#(U171(X1, X2, X3)) | → | a__U171#(mark(X1), X2, X3) | |
| a__isLNat#(fst(V1)) | → | a__U61#(a__isPLNatKind(V1), V1) | a__U141#(tt, V1, V2) | → | a__isLNat#(V1) | |
| a__isLNat#(afterNth(V1, V2)) | → | a__U41#(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | mark#(U31(X1, X2)) | → | a__U31#(mark(X1), X2) | |
| a__U102#(tt, V2) | → | a__U103#(a__isLNat(V2)) | a__isNatural#(s(V1)) | → | a__isNaturalKind#(V1) | |
| a__isNatural#(s(V1)) | → | a__U121#(a__isNaturalKind(V1), V1) | a__sel#(N, XS) | → | a__and#(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))) | |
| mark#(U142(X1, X2)) | → | mark#(X1) | a__isLNatKind#(afterNth(V1, V2)) | → | a__isNaturalKind#(V1) | |
| a__U91#(tt, V1) | → | a__isLNat#(V1) | mark#(isPLNatKind(X)) | → | a__isPLNatKind#(X) | |
| a__isPLNatKind#(splitAt(V1, V2)) | → | a__isNaturalKind#(V1) | a__tail#(cons(N, XS)) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | |
| a__fst#(pair(X, Y)) | → | a__and#(a__isLNat(X), isLNatKind(X)) | a__U142#(tt, V2) | → | a__U143#(a__isLNat(V2)) | |
| mark#(U202(X1, X2)) | → | a__U202#(mark(X1), X2) | a__U161#(tt, N) | → | mark#(N) | |
| a__U101#(tt, V1, V2) | → | a__isNatural#(V1) | mark#(U132(X1, X2)) | → | a__U132#(mark(X1), X2) | |
| mark#(U52(X1, X2)) | → | mark#(X1) | a__natsFrom#(N) | → | a__and#(a__isNatural(N), isNaturalKind(N)) | |
| a__U132#(tt, V2) | → | a__isLNat#(V2) | a__tail#(cons(N, XS)) | → | a__U211#(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | |
| mark#(isLNatKind(X)) | → | a__isLNatKind#(X) | mark#(U201(X1, X2, X3, X4)) | → | a__U201#(mark(X1), X2, X3, X4) | |
| a__natsFrom#(N) | → | a__isNatural#(N) | mark#(U92(X)) | → | mark#(X) | |
| mark#(U21(X1, X2)) | → | a__U21#(mark(X1), X2) | mark#(take(X1, X2)) | → | mark#(X2) | |
| a__isLNat#(natsFrom(V1)) | → | a__isNaturalKind#(V1) |
| a__U101(tt, V1, V2) | → | a__U102(a__isNatural(V1), V2) | a__U102(tt, V2) | → | a__U103(a__isLNat(V2)) | |
| a__U103(tt) | → | tt | a__U11(tt, N, XS) | → | a__snd(a__splitAt(mark(N), mark(XS))) | |
| a__U111(tt, V1) | → | a__U112(a__isLNat(V1)) | a__U112(tt) | → | tt | |
| a__U121(tt, V1) | → | a__U122(a__isNatural(V1)) | a__U122(tt) | → | tt | |
| a__U131(tt, V1, V2) | → | a__U132(a__isNatural(V1), V2) | a__U132(tt, V2) | → | a__U133(a__isLNat(V2)) | |
| a__U133(tt) | → | tt | a__U141(tt, V1, V2) | → | a__U142(a__isLNat(V1), V2) | |
| a__U142(tt, V2) | → | a__U143(a__isLNat(V2)) | a__U143(tt) | → | tt | |
| a__U151(tt, V1, V2) | → | a__U152(a__isNatural(V1), V2) | a__U152(tt, V2) | → | a__U153(a__isLNat(V2)) | |
| a__U153(tt) | → | tt | a__U161(tt, N) | → | cons(mark(N), natsFrom(s(N))) | |
| a__U171(tt, N, XS) | → | a__head(a__afterNth(mark(N), mark(XS))) | a__U181(tt, Y) | → | mark(Y) | |
| a__U191(tt, XS) | → | pair(nil, mark(XS)) | a__U201(tt, N, X, XS) | → | a__U202(a__splitAt(mark(N), mark(XS)), X) | |
| a__U202(pair(YS, ZS), X) | → | pair(cons(mark(X), YS), mark(ZS)) | a__U21(tt, X) | → | mark(X) | |
| a__U211(tt, XS) | → | mark(XS) | a__U221(tt, N, XS) | → | a__fst(a__splitAt(mark(N), mark(XS))) | |
| a__U31(tt, N) | → | mark(N) | a__U41(tt, V1, V2) | → | a__U42(a__isNatural(V1), V2) | |
| a__U42(tt, V2) | → | a__U43(a__isLNat(V2)) | a__U43(tt) | → | tt | |
| a__U51(tt, V1, V2) | → | a__U52(a__isNatural(V1), V2) | a__U52(tt, V2) | → | a__U53(a__isLNat(V2)) | |
| a__U53(tt) | → | tt | a__U61(tt, V1) | → | a__U62(a__isPLNat(V1)) | |
| a__U62(tt) | → | tt | a__U71(tt, V1) | → | a__U72(a__isNatural(V1)) | |
| a__U72(tt) | → | tt | a__U81(tt, V1) | → | a__U82(a__isPLNat(V1)) | |
| a__U82(tt) | → | tt | a__U91(tt, V1) | → | a__U92(a__isLNat(V1)) | |
| a__U92(tt) | → | tt | a__afterNth(N, XS) | → | a__U11(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | |
| a__and(tt, X) | → | mark(X) | a__fst(pair(X, Y)) | → | a__U21(a__and(a__and(a__isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X) | |
| a__head(cons(N, XS)) | → | a__U31(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N) | a__isLNat(nil) | → | tt | |
| a__isLNat(afterNth(V1, V2)) | → | a__U41(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | a__isLNat(cons(V1, V2)) | → | a__U51(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | |
| a__isLNat(fst(V1)) | → | a__U61(a__isPLNatKind(V1), V1) | a__isLNat(natsFrom(V1)) | → | a__U71(a__isNaturalKind(V1), V1) | |
| a__isLNat(snd(V1)) | → | a__U81(a__isPLNatKind(V1), V1) | a__isLNat(tail(V1)) | → | a__U91(a__isLNatKind(V1), V1) | |
| a__isLNat(take(V1, V2)) | → | a__U101(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | a__isLNatKind(nil) | → | tt | |
| a__isLNatKind(afterNth(V1, V2)) | → | a__and(a__isNaturalKind(V1), isLNatKind(V2)) | a__isLNatKind(cons(V1, V2)) | → | a__and(a__isNaturalKind(V1), isLNatKind(V2)) | |
| a__isLNatKind(fst(V1)) | → | a__isPLNatKind(V1) | a__isLNatKind(natsFrom(V1)) | → | a__isNaturalKind(V1) | |
| a__isLNatKind(snd(V1)) | → | a__isPLNatKind(V1) | a__isLNatKind(tail(V1)) | → | a__isLNatKind(V1) | |
| a__isLNatKind(take(V1, V2)) | → | a__and(a__isNaturalKind(V1), isLNatKind(V2)) | a__isNatural(0) | → | tt | |
| a__isNatural(head(V1)) | → | a__U111(a__isLNatKind(V1), V1) | a__isNatural(s(V1)) | → | a__U121(a__isNaturalKind(V1), V1) | |
| a__isNatural(sel(V1, V2)) | → | a__U131(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | a__isNaturalKind(0) | → | tt | |
| a__isNaturalKind(head(V1)) | → | a__isLNatKind(V1) | a__isNaturalKind(s(V1)) | → | a__isNaturalKind(V1) | |
| a__isNaturalKind(sel(V1, V2)) | → | a__and(a__isNaturalKind(V1), isLNatKind(V2)) | a__isPLNat(pair(V1, V2)) | → | a__U141(a__and(a__isLNatKind(V1), isLNatKind(V2)), V1, V2) | |
| a__isPLNat(splitAt(V1, V2)) | → | a__U151(a__and(a__isNaturalKind(V1), isLNatKind(V2)), V1, V2) | a__isPLNatKind(pair(V1, V2)) | → | a__and(a__isLNatKind(V1), isLNatKind(V2)) | |
| a__isPLNatKind(splitAt(V1, V2)) | → | a__and(a__isNaturalKind(V1), isLNatKind(V2)) | a__natsFrom(N) | → | a__U161(a__and(a__isNatural(N), isNaturalKind(N)), N) | |
| a__sel(N, XS) | → | a__U171(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | a__snd(pair(X, Y)) | → | a__U181(a__and(a__and(a__isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y) | |
| a__splitAt(0, XS) | → | a__U191(a__and(a__isLNat(XS), isLNatKind(XS)), XS) | a__splitAt(s(N), cons(X, XS)) | → | a__U201(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)))), N, X, XS) | |
| a__tail(cons(N, XS)) | → | a__U211(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), XS) | a__take(N, XS) | → | a__U221(a__and(a__and(a__isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS))), N, XS) | |
| mark(U101(X1, X2, X3)) | → | a__U101(mark(X1), X2, X3) | mark(U102(X1, X2)) | → | a__U102(mark(X1), X2) | |
| mark(isNatural(X)) | → | a__isNatural(X) | mark(U103(X)) | → | a__U103(mark(X)) | |
| mark(isLNat(X)) | → | a__isLNat(X) | mark(U11(X1, X2, X3)) | → | a__U11(mark(X1), X2, X3) | |
| mark(snd(X)) | → | a__snd(mark(X)) | mark(splitAt(X1, X2)) | → | a__splitAt(mark(X1), mark(X2)) | |
| mark(U111(X1, X2)) | → | a__U111(mark(X1), X2) | mark(U112(X)) | → | a__U112(mark(X)) | |
| mark(U121(X1, X2)) | → | a__U121(mark(X1), X2) | mark(U122(X)) | → | a__U122(mark(X)) | |
| mark(U131(X1, X2, X3)) | → | a__U131(mark(X1), X2, X3) | mark(U132(X1, X2)) | → | a__U132(mark(X1), X2) | |
| mark(U133(X)) | → | a__U133(mark(X)) | mark(U141(X1, X2, X3)) | → | a__U141(mark(X1), X2, X3) | |
| mark(U142(X1, X2)) | → | a__U142(mark(X1), X2) | mark(U143(X)) | → | a__U143(mark(X)) | |
| mark(U151(X1, X2, X3)) | → | a__U151(mark(X1), X2, X3) | mark(U152(X1, X2)) | → | a__U152(mark(X1), X2) | |
| mark(U153(X)) | → | a__U153(mark(X)) | mark(U161(X1, X2)) | → | a__U161(mark(X1), X2) | |
| mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | mark(U171(X1, X2, X3)) | → | a__U171(mark(X1), X2, X3) | |
| mark(head(X)) | → | a__head(mark(X)) | mark(afterNth(X1, X2)) | → | a__afterNth(mark(X1), mark(X2)) | |
| mark(U181(X1, X2)) | → | a__U181(mark(X1), X2) | mark(U191(X1, X2)) | → | a__U191(mark(X1), X2) | |
| mark(U201(X1, X2, X3, X4)) | → | a__U201(mark(X1), X2, X3, X4) | mark(U202(X1, X2)) | → | a__U202(mark(X1), X2) | |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | mark(U211(X1, X2)) | → | a__U211(mark(X1), X2) | |
| mark(U221(X1, X2, X3)) | → | a__U221(mark(X1), X2, X3) | mark(fst(X)) | → | a__fst(mark(X)) | |
| mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) | mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | |
| mark(U42(X1, X2)) | → | a__U42(mark(X1), X2) | mark(U43(X)) | → | a__U43(mark(X)) | |
| mark(U51(X1, X2, X3)) | → | a__U51(mark(X1), X2, X3) | mark(U52(X1, X2)) | → | a__U52(mark(X1), X2) | |
| mark(U53(X)) | → | a__U53(mark(X)) | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) | |
| mark(U62(X)) | → | a__U62(mark(X)) | mark(isPLNat(X)) | → | a__isPLNat(X) | |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | mark(U72(X)) | → | a__U72(mark(X)) | |
| mark(U81(X1, X2)) | → | a__U81(mark(X1), X2) | mark(U82(X)) | → | a__U82(mark(X)) | |
| mark(U91(X1, X2)) | → | a__U91(mark(X1), X2) | mark(U92(X)) | → | a__U92(mark(X)) | |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | mark(isNaturalKind(X)) | → | a__isNaturalKind(X) | |
| mark(isLNatKind(X)) | → | a__isLNatKind(X) | mark(isPLNatKind(X)) | → | a__isPLNatKind(X) | |
| mark(tail(X)) | → | a__tail(mark(X)) | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | |
| mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | mark(tt) | → | tt | |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | mark(s(X)) | → | s(mark(X)) | |
| mark(pair(X1, X2)) | → | pair(mark(X1), mark(X2)) | mark(nil) | → | nil | |
| mark(0) | → | 0 | a__U101(X1, X2, X3) | → | U101(X1, X2, X3) | |
| a__U102(X1, X2) | → | U102(X1, X2) | a__isNatural(X) | → | isNatural(X) | |
| a__U103(X) | → | U103(X) | a__isLNat(X) | → | isLNat(X) | |
| a__U11(X1, X2, X3) | → | U11(X1, X2, X3) | a__snd(X) | → | snd(X) | |
| a__splitAt(X1, X2) | → | splitAt(X1, X2) | a__U111(X1, X2) | → | U111(X1, X2) | |
| a__U112(X) | → | U112(X) | a__U121(X1, X2) | → | U121(X1, X2) | |
| a__U122(X) | → | U122(X) | a__U131(X1, X2, X3) | → | U131(X1, X2, X3) | |
| a__U132(X1, X2) | → | U132(X1, X2) | a__U133(X) | → | U133(X) | |
| a__U141(X1, X2, X3) | → | U141(X1, X2, X3) | a__U142(X1, X2) | → | U142(X1, X2) | |
| a__U143(X) | → | U143(X) | a__U151(X1, X2, X3) | → | U151(X1, X2, X3) | |
| a__U152(X1, X2) | → | U152(X1, X2) | a__U153(X) | → | U153(X) | |
| a__U161(X1, X2) | → | U161(X1, X2) | a__natsFrom(X) | → | natsFrom(X) | |
| a__U171(X1, X2, X3) | → | U171(X1, X2, X3) | a__head(X) | → | head(X) | |
| a__afterNth(X1, X2) | → | afterNth(X1, X2) | a__U181(X1, X2) | → | U181(X1, X2) | |
| a__U191(X1, X2) | → | U191(X1, X2) | a__U201(X1, X2, X3, X4) | → | U201(X1, X2, X3, X4) | |
| a__U202(X1, X2) | → | U202(X1, X2) | a__U21(X1, X2) | → | U21(X1, X2) | |
| a__U211(X1, X2) | → | U211(X1, X2) | a__U221(X1, X2, X3) | → | U221(X1, X2, X3) | |
| a__fst(X) | → | fst(X) | a__U31(X1, X2) | → | U31(X1, X2) | |
| a__U41(X1, X2, X3) | → | U41(X1, X2, X3) | a__U42(X1, X2) | → | U42(X1, X2) | |
| a__U43(X) | → | U43(X) | a__U51(X1, X2, X3) | → | U51(X1, X2, X3) | |
| a__U52(X1, X2) | → | U52(X1, X2) | a__U53(X) | → | U53(X) | |
| a__U61(X1, X2) | → | U61(X1, X2) | a__U62(X) | → | U62(X) | |
| a__isPLNat(X) | → | isPLNat(X) | a__U71(X1, X2) | → | U71(X1, X2) | |
| a__U72(X) | → | U72(X) | a__U81(X1, X2) | → | U81(X1, X2) | |
| a__U82(X) | → | U82(X) | a__U91(X1, X2) | → | U91(X1, X2) | |
| a__U92(X) | → | U92(X) | a__and(X1, X2) | → | and(X1, X2) | |
| a__isNaturalKind(X) | → | isNaturalKind(X) | a__isLNatKind(X) | → | isLNatKind(X) | |
| a__isPLNatKind(X) | → | isPLNatKind(X) | a__tail(X) | → | tail(X) | |
| a__take(X1, X2) | → | take(X1, X2) | a__sel(X1, X2) | → | sel(X1, X2) |
Termination of terms over the following signature is verified: a__U121, a__U122, U112, U111, U62, U61, a__isPLNat, a__U41, a__U43, a__U42, a__isNatural, a__U191, a__isPLNatKind, a__U112, a__isLNatKind, a__U111, isPLNat, isLNatKind, tail, U71, U191, U72, 0, U122, U121, a__U31, a__sel, a__U103, a__U141, a__U142, a__U143, a__take, pair, U132, U43, U131, U42, a__U91, U41, a__U92, U133, a__fst, a__head, a__snd, a__U21, cons, a__afterNth, a__U131, a__U132, a__U133, splitAt, U143, U142, U141, U51, s, tt, U53, U52, a__U11, afterNth, natsFrom, a__natsFrom, U161, a__U161, fst, U211, a__U221, a__U72, a__U71, head, U21, a__U202, U153, mark, U151, U152, a__U153, a__U152, a__U151, and, isPLNatKind, U221, a__U211, isLNat, a__U82, a__U81, U31, a__U51, U181, a__U52, a__U53, isNatural, a__U181, a__and, a__U201, a__isNaturalKind, U92, U91, a__isLNat, a__U102, a__U101, snd, isNaturalKind, U171, a__U62, a__U171, a__tail, U201, U202, a__splitAt, U82, take, U81, U11, a__U61, U102, sel, U103, nil, U101