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)].
| U261#(tt, V2) | → | activate#(V2) | U72#(tt, V1) | → | activate#(V1) | |
| afterNth#(N, XS) | → | isNatural#(N) | isNatural#(n__sel(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U53#(tt, V1, V2) | → | activate#(V2) | U81#(tt, V1) | → | isPLNatKind#(activate(V1)) | |
| U294#(tt, N, XS) | → | activate#(XS) | U326#(tt, N, X, XS) | → | U327#(splitAt(activate(N), activate(XS)), activate(X)) | |
| isLNat#(n__cons(V1, V2)) | → | U51#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U343#(tt, N, XS) | → | activate#(N) | |
| U34#(tt, N) | → | activate#(N) | U344#(tt, N, XS) | → | activate#(N) | |
| U244#(tt, V1, V2) | → | isLNat#(activate(V1)) | U23#(tt, X, Y) | → | activate#(X) | |
| U91#(tt, V1) | → | activate#(V1) | U171#(tt, V2) | → | activate#(V2) | |
| U331#(tt, N, XS) | → | U332#(isNaturalKind(activate(N)), activate(XS)) | activate#(n__head(X)) | → | head#(X) | |
| U252#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | isLNat#(n__afterNth(V1, V2)) | → | U41#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| U342#(tt, N, XS) | → | activate#(N) | U301#(tt, X, Y) | → | U302#(isLNatKind(activate(X)), activate(Y)) | |
| U44#(tt, V1, V2) | → | isNatural#(activate(V1)) | U33#(tt, N, XS) | → | U34#(isLNatKind(activate(XS)), activate(N)) | |
| isNaturalKind#(n__head(V1)) | → | isLNatKind#(activate(V1)) | U253#(tt, V1, V2) | → | activate#(V1) | |
| U322#(tt, N, X, XS) | → | activate#(XS) | U245#(tt, V2) | → | isLNat#(activate(V2)) | |
| isPLNatKind#(n__pair(V1, V2)) | → | activate#(V2) | U293#(tt, N, XS) | → | isLNatKind#(activate(XS)) | |
| U192#(tt, V1) | → | activate#(V1) | U241#(tt, V1, V2) | → | isLNatKind#(activate(V1)) | |
| U254#(tt, V1, V2) | → | activate#(V1) | U102#(tt, V1, V2) | → | activate#(V1) | |
| U105#(tt, V2) | → | activate#(V2) | isLNatKind#(n__afterNth(V1, V2)) | → | U111#(isNaturalKind(activate(V1)), activate(V2)) | |
| activate#(n__sel(X1, X2)) | → | sel#(X1, X2) | isPLNatKind#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| U281#(tt, N) | → | activate#(N) | U253#(tt, V1, V2) | → | U254#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U181#(tt, V1) | → | activate#(V1) | isLNatKind#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| U242#(tt, V1, V2) | → | activate#(V2) | U302#(tt, Y) | → | activate#(Y) | |
| U204#(tt, V1, V2) | → | U205#(isNatural(activate(V1)), activate(V2)) | U342#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U53#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | U327#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| U312#(tt, XS) | → | pair#(nil, activate(XS)) | U52#(tt, V1, V2) | → | activate#(V2) | |
| U294#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | isPLNatKind#(n__pair(V1, V2)) | → | U261#(isLNatKind(activate(V1)), activate(V2)) | |
| U192#(tt, V1) | → | U193#(isNatural(activate(V1))) | take#(N, XS) | → | isNatural#(N) | |
| U281#(tt, N) | → | isNaturalKind#(activate(N)) | U182#(tt, V1) | → | U183#(isLNat(activate(V1))) | |
| U51#(tt, V1, V2) | → | U52#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U111#(tt, V2) | → | activate#(V2) | |
| U325#(tt, N, X, XS) | → | activate#(XS) | U202#(tt, V1, V2) | → | activate#(V1) | |
| U23#(tt, X, Y) | → | activate#(Y) | U192#(tt, V1) | → | isNatural#(activate(V1)) | |
| U323#(tt, N, X, XS) | → | U324#(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS)) | U244#(tt, V1, V2) | → | U245#(isLNat(activate(V1)), activate(V2)) | |
| U201#(tt, V1, V2) | → | isNaturalKind#(activate(V1)) | U92#(tt, V1) | → | isLNat#(activate(V1)) | |
| U21#(tt, X, Y) | → | U22#(isLNatKind(activate(X)), activate(X), activate(Y)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| U191#(tt, V1) | → | isNaturalKind#(activate(V1)) | U331#(tt, N, XS) | → | isNaturalKind#(activate(N)) | |
| U326#(tt, N, X, XS) | → | activate#(N) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| U71#(tt, V1) | → | U72#(isNaturalKind(activate(V1)), activate(V1)) | U103#(tt, V1, V2) | → | activate#(V2) | |
| U42#(tt, V1, V2) | → | activate#(V1) | sel#(N, XS) | → | U291#(isNatural(N), N, XS) | |
| U104#(tt, V1, V2) | → | isNatural#(activate(V1)) | tail#(cons(N, XS)) | → | U331#(isNatural(N), N, activate(XS)) | |
| U241#(tt, V1, V2) | → | activate#(V2) | U327#(pair(YS, ZS), X) | → | activate#(X) | |
| U32#(tt, N, XS) | → | activate#(XS) | U103#(tt, V1, V2) | → | U104#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U171#(tt, V2) | → | isLNatKind#(activate(V2)) | U203#(tt, V1, V2) | → | activate#(V1) | |
| U33#(tt, N, XS) | → | activate#(XS) | U282#(tt, N) | → | cons#(activate(N), n__natsFrom(s(activate(N)))) | |
| U311#(tt, XS) | → | U312#(isLNatKind(activate(XS)), activate(XS)) | U191#(tt, V1) | → | U192#(isNaturalKind(activate(V1)), activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | U121#(tt, V2) | → | activate#(V2) | |
| U171#(tt, V2) | → | U172#(isLNatKind(activate(V2))) | U205#(tt, V2) | → | activate#(V2) | |
| isLNat#(n__fst(V1)) | → | activate#(V1) | splitAt#(0, XS) | → | isLNat#(XS) | |
| U243#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | U301#(tt, X, Y) | → | activate#(X) | |
| U334#(tt, XS) | → | activate#(XS) | U45#(tt, V2) | → | U46#(isLNat(activate(V2))) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | U252#(tt, V1, V2) | → | activate#(V1) | |
| isLNatKind#(n__cons(V1, V2)) | → | activate#(V1) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| isNatural#(n__s(V1)) | → | isNaturalKind#(activate(V1)) | activate#(n__fst(X)) | → | fst#(X) | |
| isLNatKind#(n__snd(V1)) | → | isPLNatKind#(activate(V1)) | U181#(tt, V1) | → | U182#(isLNatKind(activate(V1)), activate(V1)) | |
| U312#(tt, XS) | → | nil# | U12#(tt, N, XS) | → | activate#(XS) | |
| U14#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | U42#(tt, V1, V2) | → | U43#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U14#(tt, N, XS) | → | activate#(N) | sel#(N, XS) | → | isNatural#(N) | |
| U251#(tt, V1, V2) | → | U252#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | isNatural#(n__head(V1)) | → | U181#(isLNatKind(activate(V1)), activate(V1)) | |
| U344#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | U323#(tt, N, X, XS) | → | activate#(N) | |
| U13#(tt, N, XS) | → | activate#(XS) | U104#(tt, V1, V2) | → | U105#(isNatural(activate(V1)), activate(V2)) | |
| U344#(tt, N, XS) | → | activate#(XS) | U22#(tt, X, Y) | → | activate#(X) | |
| U204#(tt, V1, V2) | → | activate#(V2) | U331#(tt, N, XS) | → | activate#(XS) | |
| U291#(tt, N, XS) | → | activate#(XS) | U341#(tt, N, XS) | → | isNaturalKind#(activate(N)) | |
| isNaturalKind#(n__sel(V1, V2)) | → | U231#(isNaturalKind(activate(V1)), activate(V2)) | isLNat#(n__take(V1, V2)) | → | activate#(V1) | |
| U62#(tt, V1) | → | isPLNat#(activate(V1)) | U92#(tt, V1) | → | U93#(isLNat(activate(V1))) | |
| U281#(tt, N) | → | U282#(isNaturalKind(activate(N)), activate(N)) | U32#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | isLNat#(n__tail(V1)) | → | U91#(isLNatKind(activate(V1)), activate(V1)) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U294#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| U244#(tt, V1, V2) | → | activate#(V2) | isLNatKind#(n__cons(V1, V2)) | → | activate#(V2) | |
| U201#(tt, V1, V2) | → | activate#(V2) | U324#(tt, N, X, XS) | → | activate#(XS) | |
| U254#(tt, V1, V2) | → | activate#(V2) | isLNat#(n__snd(V1)) | → | isPLNatKind#(activate(V1)) | |
| U333#(tt, XS) | → | isLNatKind#(activate(XS)) | isLNat#(n__snd(V1)) | → | U81#(isPLNatKind(activate(V1)), activate(V1)) | |
| isLNatKind#(n__cons(V1, V2)) | → | isNaturalKind#(activate(V1)) | U291#(tt, N, XS) | → | U292#(isNaturalKind(activate(N)), activate(N), activate(XS)) | |
| U62#(tt, V1) | → | U63#(isPLNat(activate(V1))) | U33#(tt, N, XS) | → | activate#(N) | |
| isLNatKind#(n__fst(V1)) | → | isPLNatKind#(activate(V1)) | U292#(tt, N, XS) | → | U293#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | isPLNat#(n__splitAt(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U55#(tt, V2) | → | U56#(isLNat(activate(V2))) | natsFrom#(N) | → | isNatural#(N) | |
| natsFrom#(N) | → | U281#(isNatural(N), N) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | U103#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| U82#(tt, V1) | → | isPLNat#(activate(V1)) | U242#(tt, V1, V2) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | U82#(tt, V1) | → | U83#(isPLNat(activate(V1))) | |
| U332#(tt, XS) | → | U333#(isLNat(activate(XS)), activate(XS)) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| U43#(tt, V1, V2) | → | activate#(V2) | U241#(tt, V1, V2) | → | U242#(isLNatKind(activate(V1)), activate(V1), activate(V2)) | |
| U324#(tt, N, X, XS) | → | activate#(X) | U13#(tt, N, XS) | → | activate#(N) | |
| U54#(tt, V1, V2) | → | isNatural#(activate(V1)) | U91#(tt, V1) | → | isLNatKind#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | U242#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| U303#(tt, Y) | → | U304#(isLNatKind(activate(Y)), activate(Y)) | afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | |
| U51#(tt, V1, V2) | → | activate#(V1) | U241#(tt, V1, V2) | → | activate#(V1) | |
| isPLNatKind#(n__splitAt(V1, V2)) | → | isNaturalKind#(activate(V1)) | U327#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | |
| snd#(pair(X, Y)) | → | U301#(isLNat(X), X, Y) | U82#(tt, V1) | → | activate#(V1) | |
| U324#(tt, N, X, XS) | → | isLNat#(activate(XS)) | U52#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| U12#(tt, N, XS) | → | isLNat#(activate(XS)) | U333#(tt, XS) | → | activate#(XS) | |
| U321#(tt, N, X, XS) | → | activate#(N) | U53#(tt, V1, V2) | → | activate#(V1) | |
| U294#(tt, N, XS) | → | activate#(N) | U182#(tt, V1) | → | activate#(V1) | |
| U55#(tt, V2) | → | isLNat#(activate(V2)) | U321#(tt, N, X, XS) | → | activate#(XS) | |
| isLNatKind#(n__afterNth(V1, V2)) | → | activate#(V1) | U182#(tt, V1) | → | isLNat#(activate(V1)) | |
| U101#(tt, V1, V2) | → | activate#(V1) | U45#(tt, V2) | → | isLNat#(activate(V2)) | |
| U101#(tt, V1, V2) | → | isNaturalKind#(activate(V1)) | U202#(tt, V1, V2) | → | U203#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U41#(tt, V1, V2) | → | U42#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U252#(tt, V1, V2) | → | activate#(V2) | |
| isLNatKind#(n__tail(V1)) | → | activate#(V1) | isPLNatKind#(n__splitAt(V1, V2)) | → | U271#(isNaturalKind(activate(V1)), activate(V2)) | |
| U21#(tt, X, Y) | → | activate#(Y) | activate#(n__pair(X1, X2)) | → | pair#(X1, X2) | |
| U12#(tt, N, XS) | → | activate#(N) | isLNat#(n__take(V1, V2)) | → | U101#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| U301#(tt, X, Y) | → | isLNatKind#(activate(X)) | splitAt#(0, XS) | → | U311#(isLNat(XS), XS) | |
| U251#(tt, V1, V2) | → | activate#(V2) | U44#(tt, V1, V2) | → | U45#(isNatural(activate(V1)), activate(V2)) | |
| U324#(tt, N, X, XS) | → | U325#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | U14#(tt, N, XS) | → | activate#(XS) | |
| activate#(n__0) | → | 0# | U231#(tt, V2) | → | activate#(V2) | |
| U111#(tt, V2) | → | U112#(isLNatKind(activate(V2))) | tail#(cons(N, XS)) | → | activate#(XS) | |
| U21#(tt, X, Y) | → | activate#(X) | U322#(tt, N, X, XS) | → | isNatural#(activate(X)) | |
| U255#(tt, V2) | → | U256#(isLNat(activate(V2))) | U244#(tt, V1, V2) | → | activate#(V1) | |
| U101#(tt, V1, V2) | → | U102#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U54#(tt, V1, V2) | → | activate#(V2) | |
| U101#(tt, V1, V2) | → | activate#(V2) | U243#(tt, V1, V2) | → | U244#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U41#(tt, V1, V2) | → | isNaturalKind#(activate(V1)) | U341#(tt, N, XS) | → | activate#(XS) | |
| U81#(tt, V1) | → | activate#(V1) | activate#(n__cons(X1, X2)) | → | cons#(X1, X2) | |
| U271#(tt, V2) | → | activate#(V2) | U42#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| isLNatKind#(n__take(V1, V2)) | → | activate#(V1) | U14#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U24#(tt, X) | → | activate#(X) | U245#(tt, V2) | → | activate#(V2) | |
| U312#(tt, XS) | → | activate#(XS) | U204#(tt, V1, V2) | → | isNatural#(activate(V1)) | |
| isNatural#(n__head(V1)) | → | isLNatKind#(activate(V1)) | U43#(tt, V1, V2) | → | activate#(V1) | |
| U252#(tt, V1, V2) | → | U253#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U62#(tt, V1) | → | activate#(V1) | |
| U23#(tt, X, Y) | → | U24#(isLNatKind(activate(Y)), activate(X)) | isPLNat#(n__pair(V1, V2)) | → | U241#(isLNatKind(activate(V1)), activate(V1), activate(V2)) | |
| splitAt#(s(N), cons(X, XS)) | → | U321#(isNatural(N), N, X, activate(XS)) | isLNatKind#(n__natsFrom(V1)) | → | isNaturalKind#(activate(V1)) | |
| U311#(tt, XS) | → | activate#(XS) | U321#(tt, N, X, XS) | → | U322#(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS)) | |
| U55#(tt, V2) | → | activate#(V2) | U22#(tt, X, Y) | → | U23#(isLNat(activate(Y)), activate(X), activate(Y)) | |
| isLNat#(n__natsFrom(V1)) | → | U71#(isNaturalKind(activate(V1)), activate(V1)) | U254#(tt, V1, V2) | → | isNatural#(activate(V1)) | |
| isNaturalKind#(n__sel(V1, V2)) | → | activate#(V2) | U282#(tt, N) | → | activate#(N) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V2) | isLNatKind#(n__tail(V1)) | → | isLNatKind#(activate(V1)) | |
| U191#(tt, V1) | → | activate#(V1) | U102#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | isPLNatKind#(n__pair(V1, V2)) | → | isLNatKind#(activate(V1)) | |
| U322#(tt, N, X, XS) | → | U323#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U302#(tt, Y) | → | U303#(isLNat(activate(Y)), activate(Y)) | |
| U333#(tt, XS) | → | U334#(isLNatKind(activate(XS)), activate(XS)) | U105#(tt, V2) | → | U106#(isLNat(activate(V2))) | |
| U11#(tt, N, XS) | → | U12#(isNaturalKind(activate(N)), activate(N), activate(XS)) | isLNatKind#(n__afterNth(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| isNaturalKind#(n__s(V1)) | → | U221#(isNaturalKind(activate(V1))) | U33#(tt, N, XS) | → | isLNatKind#(activate(XS)) | |
| U22#(tt, X, Y) | → | isLNat#(activate(Y)) | isNaturalKind#(n__sel(V1, V2)) | → | activate#(V1) | |
| U81#(tt, V1) | → | U82#(isPLNatKind(activate(V1)), activate(V1)) | U72#(tt, V1) | → | isNatural#(activate(V1)) | |
| U11#(tt, N, XS) | → | isNaturalKind#(activate(N)) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| U342#(tt, N, XS) | → | activate#(XS) | U102#(tt, V1, V2) | → | activate#(V2) | |
| isLNatKind#(n__natsFrom(V1)) | → | U141#(isNaturalKind(activate(V1))) | isLNat#(n__natsFrom(V1)) | → | isNaturalKind#(activate(V1)) | |
| U321#(tt, N, X, XS) | → | isNaturalKind#(activate(N)) | U261#(tt, V2) | → | U262#(isLNatKind(activate(V2))) | |
| U251#(tt, V1, V2) | → | isNaturalKind#(activate(V1)) | isNaturalKind#(n__s(V1)) | → | isNaturalKind#(activate(V1)) | |
| isLNat#(n__fst(V1)) | → | U61#(isPLNatKind(activate(V1)), activate(V1)) | head#(cons(N, XS)) | → | isNatural#(N) | |
| U32#(tt, N, XS) | → | U33#(isLNat(activate(XS)), activate(N), activate(XS)) | activate#(n__afterNth(X1, X2)) | → | afterNth#(X1, X2) | |
| U202#(tt, V1, V2) | → | activate#(V2) | U12#(tt, N, XS) | → | U13#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| activate#(n__take(X1, X2)) | → | take#(X1, X2) | U292#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U271#(tt, V2) | → | isLNatKind#(activate(V2)) | U13#(tt, N, XS) | → | U14#(isLNatKind(activate(XS)), activate(N), activate(XS)) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | U104#(tt, V1, V2) | → | activate#(V2) | |
| U181#(tt, V1) | → | isLNatKind#(activate(V1)) | U72#(tt, V1) | → | U73#(isNatural(activate(V1))) | |
| isLNatKind#(n__take(V1, V2)) | → | activate#(V2) | U322#(tt, N, X, XS) | → | activate#(X) | |
| U121#(tt, V2) | → | isLNatKind#(activate(V2)) | U45#(tt, V2) | → | activate#(V2) | |
| U54#(tt, V1, V2) | → | U55#(isNatural(activate(V1)), activate(V2)) | isLNat#(n__tail(V1)) | → | isLNatKind#(activate(V1)) | |
| U44#(tt, V1, V2) | → | activate#(V1) | U302#(tt, Y) | → | isLNat#(activate(Y)) | |
| U242#(tt, V1, V2) | → | U243#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U251#(tt, V1, V2) | → | activate#(V1) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | U205#(tt, V2) | → | U206#(isLNat(activate(V2))) | |
| isLNatKind#(n__snd(V1)) | → | activate#(V1) | U292#(tt, N, XS) | → | activate#(XS) | |
| U324#(tt, N, X, XS) | → | activate#(N) | U52#(tt, V1, V2) | → | activate#(V1) | |
| U54#(tt, V1, V2) | → | activate#(V1) | U13#(tt, N, XS) | → | isLNatKind#(activate(XS)) | |
| isNaturalKind#(n__head(V1)) | → | U211#(isLNatKind(activate(V1))) | isLNatKind#(n__tail(V1)) | → | U161#(isLNatKind(activate(V1))) | |
| take#(N, XS) | → | U341#(isNatural(N), N, XS) | U344#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U325#(tt, N, X, XS) | → | activate#(N) | U42#(tt, V1, V2) | → | activate#(V2) | |
| U261#(tt, V2) | → | isLNatKind#(activate(V2)) | U103#(tt, V1, V2) | → | activate#(V1) | |
| U325#(tt, N, X, XS) | → | isLNatKind#(activate(XS)) | U43#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| U323#(tt, N, X, XS) | → | activate#(X) | isLNatKind#(n__take(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U31#(tt, N, XS) | → | activate#(XS) | U253#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| U321#(tt, N, X, XS) | → | activate#(X) | U292#(tt, N, XS) | → | activate#(N) | |
| U323#(tt, N, X, XS) | → | isNaturalKind#(activate(X)) | U104#(tt, V1, V2) | → | activate#(V1) | |
| U271#(tt, V2) | → | U272#(isLNatKind(activate(V2))) | U326#(tt, N, X, XS) | → | activate#(XS) | |
| U52#(tt, V1, V2) | → | U53#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U11#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, V1, V2) | → | U204#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U243#(tt, V1, V2) | → | activate#(V2) | |
| U21#(tt, X, Y) | → | isLNatKind#(activate(X)) | U61#(tt, V1) | → | isPLNatKind#(activate(V1)) | |
| isNatural#(n__s(V1)) | → | U191#(isNaturalKind(activate(V1)), activate(V1)) | isPLNat#(n__splitAt(V1, V2)) | → | U251#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| U203#(tt, V1, V2) | → | activate#(V2) | isPLNatKind#(n__pair(V1, V2)) | → | activate#(V1) | |
| U343#(tt, N, XS) | → | activate#(XS) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| U293#(tt, N, XS) | → | activate#(N) | fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | |
| U31#(tt, N, XS) | → | isNaturalKind#(activate(N)) | isLNatKind#(n__fst(V1)) | → | U131#(isPLNatKind(activate(V1))) | |
| activate#(n__snd(X)) | → | snd#(X) | U61#(tt, V1) | → | U62#(isPLNatKind(activate(V1)), activate(V1)) | |
| U201#(tt, V1, V2) | → | activate#(V1) | U32#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U293#(tt, N, XS) | → | activate#(XS) | head#(cons(N, XS)) | → | activate#(XS) | |
| U303#(tt, Y) | → | activate#(Y) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| U43#(tt, V1, V2) | → | U44#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U303#(tt, Y) | → | isLNatKind#(activate(Y)) | |
| U326#(tt, N, X, XS) | → | activate#(X) | activate#(n__splitAt(X1, X2)) | → | splitAt#(X1, X2) | |
| U92#(tt, V1) | → | activate#(V1) | isLNatKind#(n__cons(V1, V2)) | → | U121#(isNaturalKind(activate(V1)), activate(V2)) | |
| U332#(tt, XS) | → | isLNat#(activate(XS)) | U91#(tt, V1) | → | U92#(isLNatKind(activate(V1)), activate(V1)) | |
| activate#(n__tail(X)) | → | tail#(X) | isPLNat#(n__pair(V1, V2)) | → | isLNatKind#(activate(V1)) | |
| U332#(tt, XS) | → | activate#(XS) | U342#(tt, N, XS) | → | U343#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isLNatKind#(n__natsFrom(V1)) | → | activate#(V1) | isLNatKind#(n__take(V1, V2)) | → | U171#(isNaturalKind(activate(V1)), activate(V2)) | |
| U255#(tt, V2) | → | activate#(V2) | U111#(tt, V2) | → | isLNatKind#(activate(V2)) | |
| isNaturalKind#(n__sel(V1, V2)) | → | isNaturalKind#(activate(V1)) | U121#(tt, V2) | → | U122#(isLNatKind(activate(V2))) | |
| U22#(tt, X, Y) | → | activate#(Y) | U202#(tt, V1, V2) | → | isLNatKind#(activate(V2)) | |
| U311#(tt, XS) | → | isLNatKind#(activate(XS)) | isLNat#(n__afterNth(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U41#(tt, V1, V2) | → | activate#(V2) | U282#(tt, N) | → | s#(activate(N)) | |
| U201#(tt, V1, V2) | → | U202#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U51#(tt, V1, V2) | → | isNaturalKind#(activate(V1)) | |
| isLNatKind#(n__snd(V1)) | → | U151#(isPLNatKind(activate(V1))) | U44#(tt, V1, V2) | → | activate#(V2) | |
| U11#(tt, N, XS) | → | activate#(XS) | U326#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U231#(tt, V2) | → | U232#(isLNatKind(activate(V2))) | U245#(tt, V2) | → | U246#(isLNat(activate(V2))) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | U343#(tt, N, XS) | → | U344#(isLNatKind(activate(XS)), activate(N), activate(XS)) | |
| U343#(tt, N, XS) | → | isLNatKind#(activate(XS)) | U341#(tt, N, XS) | → | activate#(N) | |
| U291#(tt, N, XS) | → | isNaturalKind#(activate(N)) | U291#(tt, N, XS) | → | activate#(N) | |
| isPLNatKind#(n__splitAt(V1, V2)) | → | activate#(V2) | U323#(tt, N, X, XS) | → | activate#(XS) | |
| U31#(tt, N, XS) | → | activate#(N) | isLNat#(n__fst(V1)) | → | isPLNatKind#(activate(V1)) | |
| U53#(tt, V1, V2) | → | U54#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U105#(tt, V2) | → | isLNat#(activate(V2)) | |
| U255#(tt, V2) | → | isLNat#(activate(V2)) | isLNat#(n__take(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U325#(tt, N, X, XS) | → | U326#(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS)) | U41#(tt, V1, V2) | → | activate#(V1) | |
| U102#(tt, V1, V2) | → | U103#(isLNatKind(activate(V2)), activate(V1), activate(V2)) | isLNatKind#(n__fst(V1)) | → | activate#(V1) | |
| U205#(tt, V2) | → | isLNat#(activate(V2)) | U331#(tt, N, XS) | → | activate#(N) | |
| U23#(tt, X, Y) | → | isLNatKind#(activate(Y)) | U322#(tt, N, X, XS) | → | activate#(N) | |
| isNaturalKind#(n__head(V1)) | → | activate#(V1) | U51#(tt, V1, V2) | → | activate#(V2) | |
| U301#(tt, X, Y) | → | activate#(Y) | U231#(tt, V2) | → | isLNatKind#(activate(V2)) | |
| isNatural#(n__sel(V1, V2)) | → | U201#(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U253#(tt, V1, V2) | → | activate#(V2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | U293#(tt, N, XS) | → | U294#(isLNatKind(activate(XS)), activate(N), activate(XS)) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | U304#(tt, Y) | → | activate#(Y) | |
| U204#(tt, V1, V2) | → | activate#(V1) | U61#(tt, V1) | → | activate#(V1) | |
| U243#(tt, V1, V2) | → | activate#(V1) | U71#(tt, V1) | → | activate#(V1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(X) | isNaturalKind#(n__s(V1)) | → | activate#(V1) | |
| U341#(tt, N, XS) | → | U342#(isNaturalKind(activate(N)), activate(N), activate(XS)) | isLNat#(n__cons(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| activate#(n__s(X)) | → | s#(X) | activate#(n__nil) | → | nil# | |
| U31#(tt, N, XS) | → | U32#(isNaturalKind(activate(N)), activate(N), activate(XS)) | U254#(tt, V1, V2) | → | U255#(isNatural(activate(V1)), activate(V2)) | |
| U71#(tt, V1) | → | isNaturalKind#(activate(V1)) | U325#(tt, N, X, XS) | → | activate#(X) |
| U101(tt, V1, V2) | → | U102(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U102(tt, V1, V2) | → | U103(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U103(tt, V1, V2) | → | U104(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U104(tt, V1, V2) | → | U105(isNatural(activate(V1)), activate(V2)) | |
| U105(tt, V2) | → | U106(isLNat(activate(V2))) | U106(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isNaturalKind(activate(N)), activate(N), activate(XS)) | U111(tt, V2) | → | U112(isLNatKind(activate(V2))) | |
| U112(tt) | → | tt | U12(tt, N, XS) | → | U13(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U121(tt, V2) | → | U122(isLNatKind(activate(V2))) | U122(tt) | → | tt | |
| U13(tt, N, XS) | → | U14(isLNatKind(activate(XS)), activate(N), activate(XS)) | U131(tt) | → | tt | |
| U14(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U141(tt) | → | tt | |
| U151(tt) | → | tt | U161(tt) | → | tt | |
| U171(tt, V2) | → | U172(isLNatKind(activate(V2))) | U172(tt) | → | tt | |
| U181(tt, V1) | → | U182(isLNatKind(activate(V1)), activate(V1)) | U182(tt, V1) | → | U183(isLNat(activate(V1))) | |
| U183(tt) | → | tt | U191(tt, V1) | → | U192(isNaturalKind(activate(V1)), activate(V1)) | |
| U192(tt, V1) | → | U193(isNatural(activate(V1))) | U193(tt) | → | tt | |
| U201(tt, V1, V2) | → | U202(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U202(tt, V1, V2) | → | U203(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U203(tt, V1, V2) | → | U204(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U204(tt, V1, V2) | → | U205(isNatural(activate(V1)), activate(V2)) | |
| U205(tt, V2) | → | U206(isLNat(activate(V2))) | U206(tt) | → | tt | |
| U21(tt, X, Y) | → | U22(isLNatKind(activate(X)), activate(X), activate(Y)) | U211(tt) | → | tt | |
| U22(tt, X, Y) | → | U23(isLNat(activate(Y)), activate(X), activate(Y)) | U221(tt) | → | tt | |
| U23(tt, X, Y) | → | U24(isLNatKind(activate(Y)), activate(X)) | U231(tt, V2) | → | U232(isLNatKind(activate(V2))) | |
| U232(tt) | → | tt | U24(tt, X) | → | activate(X) | |
| U241(tt, V1, V2) | → | U242(isLNatKind(activate(V1)), activate(V1), activate(V2)) | U242(tt, V1, V2) | → | U243(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U243(tt, V1, V2) | → | U244(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U244(tt, V1, V2) | → | U245(isLNat(activate(V1)), activate(V2)) | |
| U245(tt, V2) | → | U246(isLNat(activate(V2))) | U246(tt) | → | tt | |
| U251(tt, V1, V2) | → | U252(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | U252(tt, V1, V2) | → | U253(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U253(tt, V1, V2) | → | U254(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U254(tt, V1, V2) | → | U255(isNatural(activate(V1)), activate(V2)) | |
| U255(tt, V2) | → | U256(isLNat(activate(V2))) | U256(tt) | → | tt | |
| U261(tt, V2) | → | U262(isLNatKind(activate(V2))) | U262(tt) | → | tt | |
| U271(tt, V2) | → | U272(isLNatKind(activate(V2))) | U272(tt) | → | tt | |
| U281(tt, N) | → | U282(isNaturalKind(activate(N)), activate(N)) | U282(tt, N) | → | cons(activate(N), n__natsFrom(s(activate(N)))) | |
| U291(tt, N, XS) | → | U292(isNaturalKind(activate(N)), activate(N), activate(XS)) | U292(tt, N, XS) | → | U293(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U293(tt, N, XS) | → | U294(isLNatKind(activate(XS)), activate(N), activate(XS)) | U294(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U301(tt, X, Y) | → | U302(isLNatKind(activate(X)), activate(Y)) | U302(tt, Y) | → | U303(isLNat(activate(Y)), activate(Y)) | |
| U303(tt, Y) | → | U304(isLNatKind(activate(Y)), activate(Y)) | U304(tt, Y) | → | activate(Y) | |
| U31(tt, N, XS) | → | U32(isNaturalKind(activate(N)), activate(N), activate(XS)) | U311(tt, XS) | → | U312(isLNatKind(activate(XS)), activate(XS)) | |
| U312(tt, XS) | → | pair(nil, activate(XS)) | U32(tt, N, XS) | → | U33(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U321(tt, N, X, XS) | → | U322(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS)) | U322(tt, N, X, XS) | → | U323(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| U323(tt, N, X, XS) | → | U324(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS)) | U324(tt, N, X, XS) | → | U325(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U325(tt, N, X, XS) | → | U326(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS)) | U326(tt, N, X, XS) | → | U327(splitAt(activate(N), activate(XS)), activate(X)) | |
| U327(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | U33(tt, N, XS) | → | U34(isLNatKind(activate(XS)), activate(N)) | |
| U331(tt, N, XS) | → | U332(isNaturalKind(activate(N)), activate(XS)) | U332(tt, XS) | → | U333(isLNat(activate(XS)), activate(XS)) | |
| U333(tt, XS) | → | U334(isLNatKind(activate(XS)), activate(XS)) | U334(tt, XS) | → | activate(XS) | |
| U34(tt, N) | → | activate(N) | U341(tt, N, XS) | → | U342(isNaturalKind(activate(N)), activate(N), activate(XS)) | |
| U342(tt, N, XS) | → | U343(isLNat(activate(XS)), activate(N), activate(XS)) | U343(tt, N, XS) | → | U344(isLNatKind(activate(XS)), activate(N), activate(XS)) | |
| U344(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U41(tt, V1, V2) | → | U42(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| U42(tt, V1, V2) | → | U43(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U43(tt, V1, V2) | → | U44(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U44(tt, V1, V2) | → | U45(isNatural(activate(V1)), activate(V2)) | U45(tt, V2) | → | U46(isLNat(activate(V2))) | |
| U46(tt) | → | tt | U51(tt, V1, V2) | → | U52(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| U52(tt, V1, V2) | → | U53(isLNatKind(activate(V2)), activate(V1), activate(V2)) | U53(tt, V1, V2) | → | U54(isLNatKind(activate(V2)), activate(V1), activate(V2)) | |
| U54(tt, V1, V2) | → | U55(isNatural(activate(V1)), activate(V2)) | U55(tt, V2) | → | U56(isLNat(activate(V2))) | |
| U56(tt) | → | tt | U61(tt, V1) | → | U62(isPLNatKind(activate(V1)), activate(V1)) | |
| U62(tt, V1) | → | U63(isPLNat(activate(V1))) | U63(tt) | → | tt | |
| U71(tt, V1) | → | U72(isNaturalKind(activate(V1)), activate(V1)) | U72(tt, V1) | → | U73(isNatural(activate(V1))) | |
| U73(tt) | → | tt | U81(tt, V1) | → | U82(isPLNatKind(activate(V1)), activate(V1)) | |
| U82(tt, V1) | → | U83(isPLNat(activate(V1))) | U83(tt) | → | tt | |
| U91(tt, V1) | → | U92(isLNatKind(activate(V1)), activate(V1)) | U92(tt, V1) | → | U93(isLNat(activate(V1))) | |
| U93(tt) | → | tt | afterNth(N, XS) | → | U11(isNatural(N), N, XS) | |
| fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | |
| isLNat(n__nil) | → | tt | isLNat(n__afterNth(V1, V2)) | → | U41(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| isLNat(n__cons(V1, V2)) | → | U51(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | isLNat(n__fst(V1)) | → | U61(isPLNatKind(activate(V1)), activate(V1)) | |
| isLNat(n__natsFrom(V1)) | → | U71(isNaturalKind(activate(V1)), activate(V1)) | isLNat(n__snd(V1)) | → | U81(isPLNatKind(activate(V1)), activate(V1)) | |
| isLNat(n__tail(V1)) | → | U91(isLNatKind(activate(V1)), activate(V1)) | isLNat(n__take(V1, V2)) | → | U101(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| isLNatKind(n__nil) | → | tt | isLNatKind(n__afterNth(V1, V2)) | → | U111(isNaturalKind(activate(V1)), activate(V2)) | |
| isLNatKind(n__cons(V1, V2)) | → | U121(isNaturalKind(activate(V1)), activate(V2)) | isLNatKind(n__fst(V1)) | → | U131(isPLNatKind(activate(V1))) | |
| isLNatKind(n__natsFrom(V1)) | → | U141(isNaturalKind(activate(V1))) | isLNatKind(n__snd(V1)) | → | U151(isPLNatKind(activate(V1))) | |
| isLNatKind(n__tail(V1)) | → | U161(isLNatKind(activate(V1))) | isLNatKind(n__take(V1, V2)) | → | U171(isNaturalKind(activate(V1)), activate(V2)) | |
| isNatural(n__0) | → | tt | isNatural(n__head(V1)) | → | U181(isLNatKind(activate(V1)), activate(V1)) | |
| isNatural(n__s(V1)) | → | U191(isNaturalKind(activate(V1)), activate(V1)) | isNatural(n__sel(V1, V2)) | → | U201(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| isNaturalKind(n__0) | → | tt | isNaturalKind(n__head(V1)) | → | U211(isLNatKind(activate(V1))) | |
| isNaturalKind(n__s(V1)) | → | U221(isNaturalKind(activate(V1))) | isNaturalKind(n__sel(V1, V2)) | → | U231(isNaturalKind(activate(V1)), activate(V2)) | |
| isPLNat(n__pair(V1, V2)) | → | U241(isLNatKind(activate(V1)), activate(V1), activate(V2)) | isPLNat(n__splitAt(V1, V2)) | → | U251(isNaturalKind(activate(V1)), activate(V1), activate(V2)) | |
| isPLNatKind(n__pair(V1, V2)) | → | U261(isLNatKind(activate(V1)), activate(V2)) | isPLNatKind(n__splitAt(V1, V2)) | → | U271(isNaturalKind(activate(V1)), activate(V2)) | |
| natsFrom(N) | → | U281(isNatural(N), N) | sel(N, XS) | → | U291(isNatural(N), N, XS) | |
| snd(pair(X, Y)) | → | U301(isLNat(X), X, Y) | splitAt(0, XS) | → | U311(isLNat(XS), XS) | |
| splitAt(s(N), cons(X, XS)) | → | U321(isNatural(N), N, X, activate(XS)) | tail(cons(N, XS)) | → | U331(isNatural(N), N, activate(XS)) | |
| take(N, XS) | → | U341(isNatural(N), N, XS) | natsFrom(X) | → | n__natsFrom(X) | |
| nil | → | n__nil | afterNth(X1, X2) | → | n__afterNth(X1, X2) | |
| cons(X1, X2) | → | n__cons(X1, X2) | fst(X) | → | n__fst(X) | |
| snd(X) | → | n__snd(X) | tail(X) | → | n__tail(X) | |
| take(X1, X2) | → | n__take(X1, X2) | 0 | → | n__0 | |
| head(X) | → | n__head(X) | s(X) | → | n__s(X) | |
| sel(X1, X2) | → | n__sel(X1, X2) | pair(X1, X2) | → | n__pair(X1, X2) | |
| splitAt(X1, X2) | → | n__splitAt(X1, X2) | activate(n__natsFrom(X)) | → | natsFrom(X) | |
| activate(n__nil) | → | nil | activate(n__afterNth(X1, X2)) | → | afterNth(X1, X2) | |
| activate(n__cons(X1, X2)) | → | cons(X1, X2) | activate(n__fst(X)) | → | fst(X) | |
| activate(n__snd(X)) | → | snd(X) | activate(n__tail(X)) | → | tail(X) | |
| activate(n__take(X1, X2)) | → | take(X1, X2) | activate(n__0) | → | 0 | |
| activate(n__head(X)) | → | head(X) | activate(n__s(X)) | → | s(X) | |
| activate(n__sel(X1, X2)) | → | sel(X1, X2) | activate(n__pair(X1, X2)) | → | pair(X1, X2) | |
| activate(n__splitAt(X1, X2)) | → | splitAt(X1, X2) | activate(X) | → | X |
Termination of terms over the following signature is verified: n__snd, U311, U312, U104, n__sel, U105, n__fst, U106, activate, U112, U63, U111, U62, U61, U303, U302, U304, U251, U253, U252, U255, U254, U256, n__tail, U322, U323, isPLNat, isLNatKind, U321, tail, U193, n__natsFrom, U192, U71, U191, U73, n__cons, U72, 0, U122, U121, U262, U261, pair, U331, U332, U333, U334, U46, U325, U45, U324, U44, U327, U43, U131, U326, U42, U41, U232, U231, cons, U341, n__take, U344, U342, splitAt, U343, U55, U54, U141, U56, U51, s, tt, U53, U52, U246, U245, U244, U243, afterNth, U242, U241, natsFrom, U161, U204, U203, U206, U205, n__s, fst, U211, n__nil, U23, head, U24, U21, U22, U294, U292, U293, U151, U291, isPLNatKind, U221, isLNat, U31, U32, U33, U34, U181, U182, U183, isNatural, n__head, n__splitAt, U281, U282, n__0, n__afterNth, U93, U92, U91, snd, U171, isNaturalKind, U172, U272, U83, U271, U201, U202, U14, take, U82, U301, U81, U11, n__pair, U12, U13, U102, sel, U103, U101, nil