The TRS could not be proven terminating. The proof attempt took 60017 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | U41#(tt, V1, V2) | → | U42#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__tail(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| isLNatKind#(n__natsFrom(V1)) | → | isNaturalKind#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U121#(tt, V1) | → | U122#(isNatural(activate(V1))) | U151#(tt, V1, V2) | → | activate#(V1) | |
| U91#(tt, V1) | → | isLNat#(activate(V1)) | head#(cons(N, XS)) | → | and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))) | |
| U191#(tt, XS) | → | pair#(nil, activate(XS)) | isLNat#(n__natsFrom(V1)) | → | U71#(isNaturalKind(activate(V1)), activate(V1)) | |
| activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) | splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__isNaturalKind(N)) | |
| isNaturalKind#(n__sel(V1, V2)) | → | activate#(V2) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNatKind#(n__tail(V1)) | → | isLNatKind#(activate(V1)) | U141#(tt, V1, V2) | → | activate#(V1) | |
| U91#(tt, V1) | → | activate#(V1) | U201#(tt, N, X, XS) | → | activate#(XS) | |
| U71#(tt, V1) | → | isNatural#(activate(V1)) | U181#(tt, Y) | → | activate#(Y) | |
| isLNatKind#(n__afterNth(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| U132#(tt, V2) | → | isLNat#(activate(V2)) | U202#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | |
| U102#(tt, V2) | → | activate#(V2) | isPLNatKind#(n__pair(V1, V2)) | → | isLNatKind#(activate(V1)) | |
| splitAt#(s(N), cons(X, XS)) | → | and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))) | isNaturalKind#(n__sel(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| U111#(tt, V1) | → | U112#(isLNat(activate(V1))) | isPLNat#(n__splitAt(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| isLNatKind#(n__afterNth(V1, V2)) | → | isNaturalKind#(activate(V1)) | U51#(tt, V1, V2) | → | U52#(isNatural(activate(V1)), activate(V2)) | |
| U221#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | U131#(tt, V1, V2) | → | activate#(V2) | |
| isNaturalKind#(n__head(V1)) | → | isLNatKind#(activate(V1)) | tail#(cons(N, XS)) | → | and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | U52#(tt, V2) | → | isLNat#(activate(V2)) | |
| activate#(n__s(X)) | → | activate#(X) | isPLNatKind#(n__pair(V1, V2)) | → | activate#(V2) | |
| isNaturalKind#(n__sel(V1, V2)) | → | activate#(V1) | isPLNat#(n__pair(V1, V2)) | → | and#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| isPLNatKind#(n__splitAt(V1, V2)) | → | activate#(V1) | isLNatKind#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | U152#(tt, V2) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | U131#(tt, V1, V2) | → | isNatural#(activate(V1)) | |
| isLNat#(n__natsFrom(V1)) | → | isNaturalKind#(activate(V1)) | activate#(n__isLNatKind(X)) | → | isLNatKind#(X) | |
| isNaturalKind#(n__s(V1)) | → | isNaturalKind#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| U81#(tt, V1) | → | U82#(isPLNat(activate(V1))) | isLNat#(n__fst(V1)) | → | U61#(isPLNatKind(activate(V1)), activate(V1)) | |
| head#(cons(N, XS)) | → | isNatural#(N) | U151#(tt, V1, V2) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | U101#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | U201#(tt, N, X, XS) | → | activate#(N) | |
| isNatural#(n__sel(V1, V2)) | → | U131#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | activate#(n__pair(X1, X2)) | → | pair#(activate(X1), activate(X2)) | |
| head#(cons(N, XS)) | → | and#(isNatural(N), n__isNaturalKind(N)) | take#(N, XS) | → | U221#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | U71#(tt, V1) | → | U72#(isNatural(activate(V1))) | |
| U52#(tt, V2) | → | U53#(isLNat(activate(V2))) | U141#(tt, V1, V2) | → | U142#(isLNat(activate(V1)), activate(V2)) | |
| isLNatKind#(n__take(V1, V2)) | → | activate#(V2) | isLNat#(n__tail(V1)) | → | isLNatKind#(activate(V1)) | |
| activate#(n__snd(X)) | → | activate#(X) | U101#(tt, V1, V2) | → | isNatural#(activate(V1)) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | U142#(tt, V2) | → | activate#(V2) | |
| U41#(tt, V1, V2) | → | isNatural#(activate(V1)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | U171#(tt, N, XS) | → | activate#(XS) | |
| U102#(tt, V2) | → | U103#(isLNat(activate(V2))) | U191#(tt, XS) | → | activate#(XS) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | isLNatKind#(n__snd(V1)) | → | activate#(V1) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | isPLNat#(n__splitAt(V1, V2)) | → | U151#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | |
| U121#(tt, V1) | → | isNatural#(activate(V1)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U111#(tt, V1) | → | isLNat#(activate(V1)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNatKind(X)) | afterNth#(N, XS) | → | U11#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) | |
| U131#(tt, V1, V2) | → | activate#(V1) | U151#(tt, V1, V2) | → | isNatural#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | U171#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| tail#(cons(N, XS)) | → | U211#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | isLNatKind#(n__take(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| snd#(pair(X, Y)) | → | U181#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) | take#(N, XS) | → | and#(isNatural(N), n__isNaturalKind(N)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X2) | |
| splitAt#(0, XS) | → | and#(isLNat(XS), n__isLNatKind(XS)) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| splitAt#(0, XS) | → | isLNat#(XS) | activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | |
| activate#(n__take(X1, X2)) | → | activate#(X2) | U11#(tt, N, XS) | → | activate#(N) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | U171#(tt, N, XS) | → | activate#(N) | |
| isLNatKind#(n__cons(V1, V2)) | → | activate#(V1) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | isLNat#(n__cons(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| isNatural#(n__s(V1)) | → | isNaturalKind#(activate(V1)) | isLNatKind#(n__snd(V1)) | → | isPLNatKind#(activate(V1)) | |
| isPLNatKind#(n__pair(V1, V2)) | → | activate#(V1) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| U111#(tt, V1) | → | activate#(V1) | U142#(tt, V2) | → | U143#(isLNat(activate(V2))) | |
| snd#(pair(X, Y)) | → | and#(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))) | isLNatKind#(n__cons(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| and#(tt, X) | → | activate#(X) | sel#(N, XS) | → | isNatural#(N) | |
| activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | activate#(n__head(X)) | → | activate#(X) | |
| isLNat#(n__afterNth(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | |
| afterNth#(N, XS) | → | and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))) | U61#(tt, V1) | → | isPLNat#(activate(V1)) | |
| U42#(tt, V2) | → | isLNat#(activate(V2)) | U161#(tt, N) | → | cons#(activate(N), n__natsFrom(n__s(activate(N)))) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V1) | U52#(tt, V2) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | activate#(XS) | isNatural#(n__s(V1)) | → | U121#(isNaturalKind(activate(V1)), activate(V1)) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | isLNat#(n__tail(V1)) | → | U91#(isLNatKind(activate(V1)), activate(V1)) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | isLNatKind#(n__cons(V1, V2)) | → | activate#(V2) | |
| activate#(n__isNatural(X)) | → | isNatural#(X) | activate#(n__isLNat(X)) | → | isLNat#(X) | |
| take#(N, XS) | → | and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))) | U102#(tt, V2) | → | isLNat#(activate(V2)) | |
| isLNat#(n__snd(V1)) | → | isPLNatKind#(activate(V1)) | splitAt#(0, XS) | → | U191#(and(isLNat(XS), n__isLNatKind(XS)), XS) | |
| U131#(tt, V1, V2) | → | U132#(isNatural(activate(V1)), activate(V2)) | sel#(N, XS) | → | U171#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) | |
| activate#(n__fst(X)) | → | activate#(X) | isLNat#(n__snd(V1)) | → | U81#(isPLNatKind(activate(V1)), activate(V1)) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNatKind#(activate(V1)) | U42#(tt, V2) | → | U43#(isLNat(activate(V2))) | |
| isLNatKind#(n__natsFrom(V1)) | → | activate#(V1) | U201#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| isLNat#(n__cons(V1, V2)) | → | U51#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | isLNatKind#(n__cons(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | natsFrom#(N) | → | U161#(and(isNatural(N), n__isNaturalKind(N)), N) | |
| afterNth#(N, XS) | → | and#(isNatural(N), n__isNaturalKind(N)) | tail#(cons(N, XS)) | → | and#(isNatural(N), n__isNaturalKind(N)) | |
| isNaturalKind#(n__sel(V1, V2)) | → | isNaturalKind#(activate(V1)) | isLNatKind#(n__fst(V1)) | → | isPLNatKind#(activate(V1)) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | isPLNat#(n__splitAt(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| U221#(tt, N, XS) | → | activate#(XS) | U202#(pair(YS, ZS), X) | → | activate#(X) | |
| U101#(tt, V1, V2) | → | U102#(isNatural(activate(V1)), activate(V2)) | natsFrom#(N) | → | isNatural#(N) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | U201#(tt, N, X, XS) | → | U202#(splitAt(activate(N), activate(XS)), activate(X)) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | U202#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| U41#(tt, V1, V2) | → | activate#(V2) | U171#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| U152#(tt, V2) | → | U153#(isLNat(activate(V2))) | U132#(tt, V2) | → | activate#(V2) | |
| U211#(tt, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| U142#(tt, V2) | → | isLNat#(activate(V2)) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNatKind(X)) | U11#(tt, N, XS) | → | activate#(XS) | |
| U141#(tt, V1, V2) | → | activate#(V2) | activate#(n__s(X)) | → | s#(activate(X)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| U51#(tt, V1, V2) | → | activate#(V1) | activate#(n__isNaturalKind(X)) | → | isNaturalKind#(X) | |
| U151#(tt, V1, V2) | → | U152#(isNatural(activate(V1)), activate(V2)) | natsFrom#(N) | → | and#(isNatural(N), n__isNaturalKind(N)) | |
| isPLNatKind#(n__splitAt(V1, V2)) | → | isNaturalKind#(activate(V1)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| fst#(pair(X, Y)) | → | U21#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) | isPLNatKind#(n__splitAt(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| U191#(tt, XS) | → | nil# | isLNatKind#(n__afterNth(V1, V2)) | → | activate#(V1) | |
| isPLNatKind#(n__splitAt(V1, V2)) | → | activate#(V2) | U101#(tt, V1, V2) | → | activate#(V1) | |
| U152#(tt, V2) | → | isLNat#(activate(V2)) | head#(cons(N, XS)) | → | U31#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) | |
| sel#(N, XS) | → | and#(isNatural(N), n__isNaturalKind(N)) | isLNat#(n__fst(V1)) | → | isPLNatKind#(activate(V1)) | |
| isLNatKind#(n__tail(V1)) | → | activate#(V1) | isLNat#(n__take(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| isLNatKind#(n__take(V1, V2)) | → | and#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | U221#(tt, N, XS) | → | activate#(N) | |
| U41#(tt, V1, V2) | → | activate#(V1) | splitAt#(s(N), cons(X, XS)) | → | U201#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) | |
| isNatural#(n__head(V1)) | → | U111#(isLNatKind(activate(V1)), activate(V1)) | isPLNat#(n__pair(V1, V2)) | → | U141#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | |
| U121#(tt, V1) | → | activate#(V1) | isLNatKind#(n__fst(V1)) | → | activate#(V1) | |
| activate#(n__pair(X1, X2)) | → | activate#(X2) | activate#(n__0) | → | 0# | |
| U81#(tt, V1) | → | isPLNat#(activate(V1)) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| U91#(tt, V1) | → | U92#(isLNat(activate(V1))) | isNaturalKind#(n__head(V1)) | → | activate#(V1) | |
| U51#(tt, V1, V2) | → | activate#(V2) | tail#(cons(N, XS)) | → | activate#(XS) | |
| U21#(tt, X) | → | activate#(X) | U101#(tt, V1, V2) | → | activate#(V2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | isPLNatKind#(n__pair(V1, V2)) | → | and#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| U201#(tt, N, X, XS) | → | activate#(X) | U42#(tt, V2) | → | activate#(V2) | |
| sel#(N, XS) | → | and#(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))) | U61#(tt, V1) | → | activate#(V1) | |
| U81#(tt, V1) | → | activate#(V1) | U71#(tt, V1) | → | activate#(V1) | |
| isLNatKind#(n__take(V1, V2)) | → | activate#(V1) | U132#(tt, V2) | → | U133#(isLNat(activate(V2))) | |
| U51#(tt, V1, V2) | → | isNatural#(activate(V1)) | isNaturalKind#(n__s(V1)) | → | activate#(V1) | |
| fst#(pair(X, Y)) | → | and#(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))) | U31#(tt, N) | → | activate#(N) | |
| isNatural#(n__head(V1)) | → | isLNatKind#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | isNaturalKind#(activate(V1)) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__nil) | → | nil# | |
| U61#(tt, V1) | → | U62#(isPLNat(activate(V1))) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| U141#(tt, V1, V2) | → | isLNat#(activate(V1)) | isLNat#(n__afterNth(V1, V2)) | → | U41#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U221#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) |
| U101(tt, V1, V2) | → | U102(isNatural(activate(V1)), activate(V2)) | U102(tt, V2) | → | U103(isLNat(activate(V2))) | |
| U103(tt) | → | tt | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U111(tt, V1) | → | U112(isLNat(activate(V1))) | U112(tt) | → | tt | |
| U121(tt, V1) | → | U122(isNatural(activate(V1))) | U122(tt) | → | tt | |
| U131(tt, V1, V2) | → | U132(isNatural(activate(V1)), activate(V2)) | U132(tt, V2) | → | U133(isLNat(activate(V2))) | |
| U133(tt) | → | tt | U141(tt, V1, V2) | → | U142(isLNat(activate(V1)), activate(V2)) | |
| U142(tt, V2) | → | U143(isLNat(activate(V2))) | U143(tt) | → | tt | |
| U151(tt, V1, V2) | → | U152(isNatural(activate(V1)), activate(V2)) | U152(tt, V2) | → | U153(isLNat(activate(V2))) | |
| U153(tt) | → | tt | U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | |
| U171(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | activate(Y) | |
| U191(tt, XS) | → | pair(nil, activate(XS)) | U201(tt, N, X, XS) | → | U202(splitAt(activate(N), activate(XS)), activate(X)) | |
| U202(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | U21(tt, X) | → | activate(X) | |
| U211(tt, XS) | → | activate(XS) | U221(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N) | → | activate(N) | U41(tt, V1, V2) | → | U42(isNatural(activate(V1)), activate(V2)) | |
| U42(tt, V2) | → | U43(isLNat(activate(V2))) | U43(tt) | → | tt | |
| U51(tt, V1, V2) | → | U52(isNatural(activate(V1)), activate(V2)) | U52(tt, V2) | → | U53(isLNat(activate(V2))) | |
| U53(tt) | → | tt | U61(tt, V1) | → | U62(isPLNat(activate(V1))) | |
| U62(tt) | → | tt | U71(tt, V1) | → | U72(isNatural(activate(V1))) | |
| U72(tt) | → | tt | U81(tt, V1) | → | U82(isPLNat(activate(V1))) | |
| U82(tt) | → | tt | U91(tt, V1) | → | U92(isLNat(activate(V1))) | |
| U92(tt) | → | tt | afterNth(N, XS) | → | U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) | |
| head(cons(N, XS)) | → | U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 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(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | isLNatKind(n__nil) | → | tt | |
| isLNatKind(n__afterNth(V1, V2)) | → | and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | isLNatKind(n__cons(V1, V2)) | → | and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| isLNatKind(n__fst(V1)) | → | isPLNatKind(activate(V1)) | isLNatKind(n__natsFrom(V1)) | → | isNaturalKind(activate(V1)) | |
| isLNatKind(n__snd(V1)) | → | isPLNatKind(activate(V1)) | isLNatKind(n__tail(V1)) | → | isLNatKind(activate(V1)) | |
| isLNatKind(n__take(V1, V2)) | → | and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNatKind(activate(V1)), activate(V1)) | isNatural(n__s(V1)) | → | U121(isNaturalKind(activate(V1)), activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | isNaturalKind(n__0) | → | tt | |
| isNaturalKind(n__head(V1)) | → | isLNatKind(activate(V1)) | isNaturalKind(n__s(V1)) | → | isNaturalKind(activate(V1)) | |
| isNaturalKind(n__sel(V1, V2)) | → | and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) | isPLNatKind(n__pair(V1, V2)) | → | and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) | |
| isPLNatKind(n__splitAt(V1, V2)) | → | and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) | natsFrom(N) | → | U161(and(isNatural(N), n__isNaturalKind(N)), N) | |
| sel(N, XS) | → | U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) | snd(pair(X, Y)) | → | U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) | |
| splitAt(0, XS) | → | U191(and(isLNat(XS), n__isLNatKind(XS)), XS) | splitAt(s(N), cons(X, XS)) | → | U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) | take(N, XS) | → | U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isNaturalKind(X) | → | n__isNaturalKind(X) | and(X1, X2) | → | n__and(X1, X2) | |
| isLNat(X) | → | n__isLNat(X) | isLNatKind(X) | → | n__isLNatKind(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) | sel(X1, X2) | → | n__sel(X1, X2) | |
| pair(X1, X2) | → | n__pair(X1, X2) | splitAt(X1, X2) | → | n__splitAt(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isNaturalKind(X)) | → | isNaturalKind(X) | |
| activate(n__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isLNat(X)) | → | isLNat(X) | |
| activate(n__isLNatKind(X)) | → | isLNatKind(X) | activate(n__nil) | → | nil | |
| activate(n__afterNth(X1, X2)) | → | afterNth(activate(X1), activate(X2)) | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) | |
| activate(n__fst(X)) | → | fst(activate(X)) | activate(n__snd(X)) | → | snd(activate(X)) | |
| activate(n__tail(X)) | → | tail(activate(X)) | activate(n__take(X1, X2)) | → | take(activate(X1), activate(X2)) | |
| activate(n__0) | → | 0 | activate(n__head(X)) | → | head(activate(X)) | |
| activate(n__sel(X1, X2)) | → | sel(activate(X1), activate(X2)) | activate(n__pair(X1, X2)) | → | pair(activate(X1), activate(X2)) | |
| activate(n__splitAt(X1, X2)) | → | splitAt(activate(X1), activate(X2)) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, n__snd, n__sel, n__fst, n__s, activate, U112, fst, U111, U62, U61, U211, n__isLNatKind, n__nil, head, U21, n__tail, U153, U151, isLNatKind, isPLNat, U152, tail, n__natsFrom, and, U71, U191, n__cons, U72, 0, isPLNatKind, U122, U121, U221, isLNat, U31, U181, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, U43, n__afterNth, n__isLNat, U42, U92, U133, U41, U91, n__isNatural, snd, cons, isNaturalKind, U171, n__isNaturalKind, n__take, splitAt, U143, U201, n__and, U142, U202, U141, s, U51, tt, take, U82, U53, U81, U52, U11, n__pair, afterNth, U102, sel, U103, U101, nil