The TRS could not be proven terminating. The proof attempt took 60002 ms.
Problem 1 was processed with processor DependencyGraph (21371ms). | – Problem 2 was processed with processor DependencyGraph (16181ms). | | – Problem 7 remains open; application of the following processors failed []. | – Problem 3 was processed with processor DependencyGraph (17084ms). | | – Problem 8 remains open; application of the following processors failed []. | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (timeout)]. | – Problem 5 remains open; application of the following processors failed [SubtermCriterion (1ms)]. | – Problem 6 remains open; application of the following processors failed [SubtermCriterion (1ms)].
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| sel#(N, XS) | → | isNatural#(N) | U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | |
| U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) | → | activate#(V1) | |
| U82#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | |
| U51#(tt, N, XS) | → | activate#(N) | take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| head#(cons(N, XS)) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | isLNat#(n__tail(V1)) | → | activate#(V1) | |
| U91#(tt, XS) | → | activate#(XS) | U81#(tt, N, X, XS) | → | activate#(N) | |
| activate#(n__isNatural(X)) | → | isNatural#(X) | activate#(n__isLNat(X)) | → | isLNat#(X) | |
| U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| activate#(n__s(X)) | → | activate#(X) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | U51#(tt, N, XS) | → | activate#(XS) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | natsFrom#(N) | → | isNatural#(N) | |
| splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | isNatural#(n__s(V1)) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | |
| take#(N, XS) | → | isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | |
| U11#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | U41#(tt, N) | → | activate#(N) | |
| activate#(n__sel(X1, X2)) | → | activate#(X1) | U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| activate#(n__snd(X)) | → | activate#(X) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__pair(X1, X2)) | → | activate#(X2) | U81#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | U82#(pair(YS, ZS), X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| natsFrom#(N) | → | U41#(isNatural(N), N) | tail#(cons(N, XS)) | → | activate#(XS) | |
| U21#(tt, X) | → | activate#(X) | U61#(tt, Y) | → | activate#(Y) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | U101#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| splitAt#(0, XS) | → | isLNat#(XS) | activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X1) | |
| activate#(n__take(X1, X2)) | → | activate#(X2) | U11#(tt, N, XS) | → | activate#(N) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U31#(tt, N) | → | activate#(N) | U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | activate#(n__splitAt(X1, X2)) | → | activate#(X2) | |
| U71#(tt, XS) | → | activate#(XS) | U101#(tt, N, XS) | → | activate#(N) | |
| U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, n__snd, n__head, n__sel, n__splitAt, n__fst, n__s, activate, fst, n__0, U61, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, tail, n__natsFrom, splitAt, and, U71, n__and, n__cons, 0, s, U51, tt, take, U82, isLNat, U81, U11, n__pair, U31, afterNth, sel, U101, nil
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| sel#(N, XS) | → | isNatural#(N) | U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | |
| U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) | → | activate#(V1) | |
| U82#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | |
| U51#(tt, N, XS) | → | activate#(N) | take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| head#(cons(N, XS)) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | isLNat#(n__tail(V1)) | → | activate#(V1) | |
| U91#(tt, XS) | → | activate#(XS) | U81#(tt, N, X, XS) | → | activate#(N) | |
| activate#(n__isNatural(X)) | → | isNatural#(X) | activate#(n__isLNat(X)) | → | isLNat#(X) | |
| U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| U82#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__s(X)) | → | activate#(X) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | |
| U51#(tt, N, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| U41#(tt, N) | → | activate#(N) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| activate#(n__natsFrom(X)) | → | activate#(X) | snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | |
| head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U81#(tt, N, X, XS) | → | activate#(X) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | |
| U82#(pair(YS, ZS), X) | → | activate#(X) | U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | natsFrom#(N) | → | U41#(isNatural(N), N) | |
| tail#(cons(N, XS)) | → | activate#(XS) | U21#(tt, X) | → | activate#(X) | |
| U61#(tt, Y) | → | activate#(Y) | isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X2) | |
| U101#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__fst(V1)) | → | activate#(V1) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X1) | U11#(tt, N, XS) | → | activate#(N) | |
| activate#(n__take(X1, X2)) | → | activate#(X2) | activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | |
| isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | U31#(tt, N) | → | activate#(N) | |
| U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | activate#(n__head(X)) | → | head#(activate(X)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X1) | splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U71#(tt, XS) | → | activate#(XS) | |
| U101#(tt, N, XS) | → | activate#(N) | U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, n__snd, n__head, n__sel, n__splitAt, n__fst, n__s, activate, fst, n__0, U61, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, tail, n__natsFrom, splitAt, and, U71, n__and, n__cons, 0, s, U51, tt, take, U82, isLNat, U81, U11, n__pair, U31, afterNth, sel, U101, nil
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | |
| splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V1) | isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | U51#(tt, N, XS) | → | activate#(N) | |
| take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | head#(cons(N, XS)) | → | activate#(XS) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U91#(tt, XS) | → | activate#(XS) | |
| activate#(n__isNatural(X)) | → | isNatural#(X) | U81#(tt, N, X, XS) | → | activate#(N) | |
| activate#(n__isLNat(X)) | → | isLNat#(X) | U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| activate#(n__fst(X)) | → | activate#(X) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| activate#(n__s(X)) | → | activate#(X) | head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | |
| U51#(tt, N, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) | → | isNatural#(N) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| U41#(tt, N) | → | cons#(activate(N), n__natsFrom(n__s(activate(N)))) | isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | |
| take#(N, XS) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | |
| U11#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | U41#(tt, N) | → | activate#(N) | |
| activate#(n__sel(X1, X2)) | → | activate#(X1) | U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| activate#(n__snd(X)) | → | activate#(X) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__pair(X1, X2)) | → | activate#(X2) | U81#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | |
| isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | U82#(pair(YS, ZS), X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| activate#(n__and(X1, X2)) | → | activate#(X1) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| natsFrom#(N) | → | U41#(isNatural(N), N) | tail#(cons(N, XS)) | → | activate#(XS) | |
| U21#(tt, X) | → | activate#(X) | U61#(tt, Y) | → | activate#(Y) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | U101#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| splitAt#(0, XS) | → | isLNat#(XS) | activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X1) | |
| U11#(tt, N, XS) | → | activate#(N) | activate#(n__take(X1, X2)) | → | activate#(X2) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U31#(tt, N) | → | activate#(N) | U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | activate#(n__splitAt(X1, X2)) | → | activate#(X2) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| U71#(tt, XS) | → | activate#(XS) | U101#(tt, N, XS) | → | activate#(N) | |
| U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, n__snd, n__head, n__sel, n__splitAt, n__fst, n__s, activate, fst, n__0, U61, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, tail, n__natsFrom, splitAt, and, U71, n__and, n__cons, 0, s, U51, tt, take, U82, isLNat, U81, U11, n__pair, U31, afterNth, sel, U101, nil
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | |
| splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V1) | isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | U51#(tt, N, XS) | → | activate#(N) | |
| take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | head#(cons(N, XS)) | → | activate#(XS) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U91#(tt, XS) | → | activate#(XS) | |
| activate#(n__isNatural(X)) | → | isNatural#(X) | U81#(tt, N, X, XS) | → | activate#(N) | |
| activate#(n__isLNat(X)) | → | isLNat#(X) | U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| activate#(n__fst(X)) | → | activate#(X) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| activate#(n__s(X)) | → | activate#(X) | head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | |
| U51#(tt, N, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| U41#(tt, N) | → | activate#(N) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| activate#(n__natsFrom(X)) | → | activate#(X) | snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | |
| head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U81#(tt, N, X, XS) | → | activate#(X) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | |
| U82#(pair(YS, ZS), X) | → | activate#(X) | U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | tail#(cons(N, XS)) | → | activate#(XS) | |
| natsFrom#(N) | → | U41#(isNatural(N), N) | U21#(tt, X) | → | activate#(X) | |
| U61#(tt, Y) | → | activate#(Y) | isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X2) | |
| U101#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__fst(V1)) | → | activate#(V1) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X1) | U11#(tt, N, XS) | → | activate#(N) | |
| activate#(n__take(X1, X2)) | → | activate#(X2) | activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | |
| isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | U31#(tt, N) | → | activate#(N) | |
| U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | activate#(n__head(X)) | → | head#(activate(X)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X1) | splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | U71#(tt, XS) | → | activate#(XS) | |
| U101#(tt, N, XS) | → | activate#(N) | U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, n__snd, n__head, n__sel, n__splitAt, n__fst, n__s, activate, fst, n__0, U61, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, tail, n__natsFrom, splitAt, and, U71, n__and, n__cons, 0, s, U51, tt, take, U82, isLNat, U81, U11, n__pair, U31, afterNth, sel, U101, nil
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | |
| U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V1) | isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| U51#(tt, N, XS) | → | activate#(N) | head#(cons(N, XS)) | → | activate#(XS) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U91#(tt, XS) | → | activate#(XS) | |
| U81#(tt, N, X, XS) | → | activate#(N) | activate#(n__isNatural(X)) | → | isNatural#(X) | |
| activate#(n__isLNat(X)) | → | isLNat#(X) | U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| activate#(n__fst(X)) | → | activate#(X) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__s(X)) | → | activate#(X) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | |
| U51#(tt, N, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) | → | isNatural#(N) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| U41#(tt, N) | → | activate#(N) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| activate#(n__natsFrom(X)) | → | activate#(X) | snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | |
| head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U81#(tt, N, X, XS) | → | activate#(X) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | U82#(pair(YS, ZS), X) | → | activate#(X) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | natsFrom#(N) | → | U41#(isNatural(N), N) | |
| tail#(cons(N, XS)) | → | activate#(XS) | U21#(tt, X) | → | activate#(X) | |
| U61#(tt, Y) | → | activate#(Y) | isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X2) | |
| U101#(tt, N, XS) | → | activate#(XS) | U71#(tt, XS) | → | pair#(nil, activate(XS)) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| splitAt#(0, XS) | → | isLNat#(XS) | activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X1) | |
| U11#(tt, N, XS) | → | activate#(N) | activate#(n__take(X1, X2)) | → | activate#(X2) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U31#(tt, N) | → | activate#(N) | U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | activate#(n__splitAt(X1, X2)) | → | activate#(X2) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| U71#(tt, XS) | → | activate#(XS) | U101#(tt, N, XS) | → | activate#(N) | |
| U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, natsFrom, isNatural, n__snd, n__head, n__sel, n__splitAt, n__fst, n__s, activate, fst, n__0, U61, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, tail, n__natsFrom, splitAt, and, U71, n__and, n__cons, 0, s, U51, tt, take, U82, isLNat, U81, U11, n__pair, U31, afterNth, sel, U101, nil
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| sel#(N, XS) | → | isNatural#(N) | U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | |
| U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) | |
| take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V2) | U82#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) | → | activate#(V1) | |
| isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | U51#(tt, N, XS) | → | activate#(N) | |
| take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | head#(cons(N, XS)) | → | activate#(XS) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U91#(tt, XS) | → | activate#(XS) | |
| U81#(tt, N, X, XS) | → | activate#(N) | activate#(n__isNatural(X)) | → | isNatural#(X) | |
| activate#(n__isLNat(X)) | → | isLNat#(X) | U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| activate#(n__fst(X)) | → | activate#(X) | U82#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| activate#(n__s(X)) | → | activate#(X) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | U51#(tt, N, XS) | → | activate#(XS) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | isNatural#(n__s(V1)) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | U41#(tt, N) | → | cons#(activate(N), n__natsFrom(n__s(activate(N)))) | |
| isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| activate#(n__pair(X1, X2)) | → | pair#(activate(X1), activate(X2)) | isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__s(X)) | → | s#(activate(X)) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| U41#(tt, N) | → | activate#(N) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| activate#(n__natsFrom(X)) | → | activate#(X) | snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | |
| head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| activate#(n__0) | → | 0# | U81#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | U82#(pair(YS, ZS), X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| tail#(cons(N, XS)) | → | activate#(XS) | natsFrom#(N) | → | U41#(isNatural(N), N) | |
| U21#(tt, X) | → | activate#(X) | isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | |
| U61#(tt, Y) | → | activate#(Y) | isNatural#(n__sel(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | U101#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | U71#(tt, XS) | → | pair#(nil, activate(XS)) | |
| isLNat#(n__fst(V1)) | → | activate#(V1) | U71#(tt, XS) | → | nil# | |
| splitAt#(0, XS) | → | isLNat#(XS) | activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X1) | |
| U11#(tt, N, XS) | → | activate#(N) | activate#(n__take(X1, X2)) | → | activate#(X2) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U31#(tt, N) | → | activate#(N) | U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| activate#(n__nil) | → | nil# | activate#(n__head(X)) | → | head#(activate(X)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X1) | splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U71#(tt, XS) | → | activate#(XS) | |
| U101#(tt, N, XS) | → | activate#(N) | U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, isNatural, natsFrom, n__snd, n__head, n__sel, n__fst, n__splitAt, fst, activate, n__s, U61, n__0, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, n__natsFrom, tail, splitAt, U71, and, n__cons, n__and, 0, U51, s, tt, U82, take, U81, isLNat, U11, n__pair, afterNth, U31, sel, nil, U101
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | sel#(N, XS) → isNatural#(N) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| U82#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isNatural#(n__s(V1)) → isNatural#(activate(V1)) |
| take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | U51#(tt, N, XS) → activate#(N) |
| head#(cons(N, XS)) → activate#(XS) | snd#(pair(X, Y)) → isLNat#(X) |
| isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) |
| isPLNat#(n__pair(V1, V2)) → activate#(V1) | isLNat#(n__tail(V1)) → activate#(V1) |
| U91#(tt, XS) → activate#(XS) | activate#(n__isNatural(X)) → isNatural#(X) |
| U81#(tt, N, X, XS) → activate#(N) | activate#(n__isLNat(X)) → isLNat#(X) |
| U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | activate#(n__fst(X)) → activate#(X) |
| U82#(pair(YS, ZS), X) → cons#(activate(X), YS) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__fst(X)) → fst#(activate(X)) | activate#(n__s(X)) → activate#(X) |
| isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) |
| U51#(tt, N, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) → activate#(V1) |
| splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) → isNatural#(N) |
| fst#(pair(X, Y)) → isLNat#(X) | sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | activate#(n__take(X1, X2)) → activate#(X1) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) |
| splitAt#(s(N), cons(X, XS)) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → activate#(XS) |
| U41#(tt, N) → activate#(N) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| activate#(n__snd(X)) → snd#(activate(X)) | activate#(n__snd(X)) → activate#(X) |
| sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | activate#(n__cons(X1, X2)) → activate#(X1) |
| U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__take(V1, V2)) → activate#(V2) | tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| isNatural#(n__sel(V1, V2)) → activate#(V2) | activate#(n__tail(X)) → tail#(activate(X)) |
| activate#(n__natsFrom(X)) → activate#(X) | snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) |
| head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) → activate#(X2) |
| U81#(tt, N, X, XS) → activate#(X) | tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) |
| isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | activate#(n__pair(X1, X2)) → activate#(X1) |
| U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) | U82#(pair(YS, ZS), X) → activate#(X) |
| activate#(n__and(X1, X2)) → activate#(X1) | afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| activate#(n__natsFrom(X)) → natsFrom#(activate(X)) | tail#(cons(N, XS)) → activate#(XS) |
| natsFrom#(N) → U41#(isNatural(N), N) | U21#(tt, X) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U61#(tt, Y) → activate#(Y) |
| isNatural#(n__sel(V1, V2)) → activate#(V1) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| U101#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| 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)) |
| isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) |
| isPLNat#(n__pair(V1, V2)) → activate#(V2) | U31#(tt, N) → activate#(N) |
| activate#(n__head(X)) → head#(activate(X)) | U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) |
| activate#(n__splitAt(X1, X2)) → activate#(X1) | splitAt#(0, XS) → U71#(isLNat(XS), XS) |
| activate#(n__splitAt(X1, X2)) → activate#(X2) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | U71#(tt, XS) → activate#(XS) |
| U101#(tt, N, XS) → activate#(N) | U81#(tt, N, X, XS) → activate#(XS) |
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| sel#(N, XS) → isNatural#(N) | U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isNatural#(n__s(V1)) → isNatural#(activate(V1)) | U51#(tt, N, XS) → activate#(N) |
| take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | head#(cons(N, XS)) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U91#(tt, XS) → activate#(XS) |
| activate#(n__isNatural(X)) → isNatural#(X) | U81#(tt, N, X, XS) → activate#(N) |
| activate#(n__isLNat(X)) → isLNat#(X) | U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__fst(X)) → fst#(activate(X)) | activate#(n__s(X)) → activate#(X) |
| isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) |
| U51#(tt, N, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) → activate#(V1) |
| natsFrom#(N) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) |
| fst#(pair(X, Y)) → isLNat#(X) | sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | head#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) |
| isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__take(X1, X2)) → activate#(X1) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| U41#(tt, N) → activate#(N) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| activate#(n__snd(X)) → snd#(activate(X)) | activate#(n__snd(X)) → activate#(X) |
| sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | activate#(n__cons(X1, X2)) → activate#(X1) |
| U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__take(V1, V2)) → activate#(V2) | tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| isNatural#(n__sel(V1, V2)) → activate#(V2) | activate#(n__tail(X)) → tail#(activate(X)) |
| activate#(n__natsFrom(X)) → activate#(X) | snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) |
| head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) → activate#(X2) |
| U81#(tt, N, X, XS) → activate#(X) | isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) |
| tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | activate#(n__pair(X1, X2)) → activate#(X1) |
| U82#(pair(YS, ZS), X) → activate#(X) | U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) |
| activate#(n__and(X1, X2)) → activate#(X1) | afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| activate#(n__natsFrom(X)) → natsFrom#(activate(X)) | tail#(cons(N, XS)) → activate#(XS) |
| natsFrom#(N) → U41#(isNatural(N), N) | U21#(tt, X) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U61#(tt, Y) → activate#(Y) |
| isNatural#(n__sel(V1, V2)) → activate#(V1) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| U101#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| U71#(tt, XS) → pair#(nil, activate(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)) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U31#(tt, N) → activate#(N) | activate#(n__head(X)) → head#(activate(X)) |
| U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| splitAt#(0, XS) → U71#(isLNat(XS), XS) | isLNat#(n__cons(V1, V2)) → activate#(V1) |
| isNatural#(n__head(V1)) → isLNat#(activate(V1)) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| U71#(tt, XS) → activate#(XS) | U101#(tt, N, XS) → activate#(N) |
| U81#(tt, N, X, XS) → activate#(XS) |
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | sel#(N, XS) → isNatural#(N) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| U82#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isNatural#(n__s(V1)) → isNatural#(activate(V1)) |
| take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | U51#(tt, N, XS) → activate#(N) |
| head#(cons(N, XS)) → activate#(XS) | snd#(pair(X, Y)) → isLNat#(X) |
| isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) |
| isPLNat#(n__pair(V1, V2)) → activate#(V1) | isLNat#(n__tail(V1)) → activate#(V1) |
| U91#(tt, XS) → activate#(XS) | activate#(n__isNatural(X)) → isNatural#(X) |
| U81#(tt, N, X, XS) → activate#(N) | activate#(n__isLNat(X)) → isLNat#(X) |
| U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | activate#(n__fst(X)) → activate#(X) |
| activate#(n__sel(X1, X2)) → activate#(X2) | activate#(n__fst(X)) → fst#(activate(X)) |
| activate#(n__s(X)) → activate#(X) | isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | U51#(tt, N, XS) → activate#(XS) |
| isLNat#(n__natsFrom(V1)) → activate#(V1) | afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| isNatural#(n__head(V1)) → activate#(V1) | splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) |
| natsFrom#(N) → isNatural#(N) | fst#(pair(X, Y)) → isLNat#(X) |
| sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | isNatural#(n__s(V1)) → activate#(V1) |
| isLNat#(n__afterNth(V1, V2)) → activate#(V2) | isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isLNat#(n__tail(V1)) → isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) |
| take#(N, XS) → isNatural#(N) | isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| head#(cons(N, XS)) → isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) → activate#(V2) |
| isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__take(X1, X2)) → activate#(X1) | isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) |
| U11#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) |
| isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) | isLNat#(n__snd(V1)) → activate#(V1) |
| snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | U41#(tt, N) → activate#(N) |
| activate#(n__sel(X1, X2)) → activate#(X1) | U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) |
| activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) | activate#(n__snd(X)) → snd#(activate(X)) |
| activate#(n__snd(X)) → activate#(X) | sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| activate#(n__cons(X1, X2)) → activate#(X1) | U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) |
| tail#(cons(N, XS)) → isNatural#(N) | isLNat#(n__take(V1, V2)) → activate#(V2) |
| tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| activate#(n__tail(X)) → tail#(activate(X)) | activate#(n__natsFrom(X)) → activate#(X) |
| snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U81#(tt, N, X, XS) → activate#(X) |
| tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) |
| activate#(n__pair(X1, X2)) → activate#(X1) | U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) |
| U82#(pair(YS, ZS), X) → activate#(X) | afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| activate#(n__and(X1, X2)) → activate#(X1) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| tail#(cons(N, XS)) → activate#(XS) | natsFrom#(N) → U41#(isNatural(N), N) |
| U21#(tt, X) → activate#(X) | isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) |
| U61#(tt, Y) → activate#(Y) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| activate#(n__afterNth(X1, X2)) → activate#(X2) | U101#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V1) | 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) |
| U11#(tt, N, XS) → activate#(N) | activate#(n__take(X1, X2)) → activate#(X2) |
| activate#(n__afterNth(X1, X2)) → afterNth#(activate(X1), activate(X2)) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U31#(tt, N) → activate#(N) | activate#(n__head(X)) → head#(activate(X)) |
| U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| splitAt#(0, XS) → U71#(isLNat(XS), XS) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| U71#(tt, XS) → activate#(XS) | U101#(tt, N, XS) → activate#(N) |
| U81#(tt, N, X, XS) → activate#(XS) |
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| sel#(N, XS) → isNatural#(N) | U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) |
| U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isNatural#(n__s(V1)) → isNatural#(activate(V1)) | take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| U51#(tt, N, XS) → activate#(N) | head#(cons(N, XS)) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U91#(tt, XS) → activate#(XS) |
| U81#(tt, N, X, XS) → activate#(N) | activate#(n__isNatural(X)) → isNatural#(X) |
| activate#(n__isLNat(X)) → isLNat#(X) | U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__s(X)) → activate#(X) | activate#(n__fst(X)) → fst#(activate(X)) |
| isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) |
| U51#(tt, N, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) → activate#(V1) |
| splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) → isNatural#(N) |
| fst#(pair(X, Y)) → isLNat#(X) | sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| head#(cons(N, XS)) → isNatural#(N) | isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | activate#(n__take(X1, X2)) → activate#(X1) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → activate#(V1) |
| isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) | snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) |
| splitAt#(s(N), cons(X, XS)) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → activate#(XS) |
| U41#(tt, N) → activate#(N) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| activate#(n__snd(X)) → snd#(activate(X)) | activate#(n__snd(X)) → activate#(X) |
| sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | activate#(n__cons(X1, X2)) → activate#(X1) |
| U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__take(V1, V2)) → activate#(V2) | tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| isNatural#(n__sel(V1, V2)) → activate#(V2) | activate#(n__tail(X)) → tail#(activate(X)) |
| activate#(n__natsFrom(X)) → activate#(X) | snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) |
| head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) → activate#(X2) |
| U81#(tt, N, X, XS) → activate#(X) | tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) |
| isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | activate#(n__pair(X1, X2)) → activate#(X1) |
| U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) | U82#(pair(YS, ZS), X) → activate#(X) |
| activate#(n__and(X1, X2)) → activate#(X1) | afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| activate#(n__natsFrom(X)) → natsFrom#(activate(X)) | natsFrom#(N) → U41#(isNatural(N), N) |
| tail#(cons(N, XS)) → activate#(XS) | U21#(tt, X) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U61#(tt, Y) → activate#(Y) |
| isNatural#(n__sel(V1, V2)) → activate#(V1) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| U101#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| 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)) |
| isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) |
| isPLNat#(n__pair(V1, V2)) → activate#(V2) | U31#(tt, N) → activate#(N) |
| activate#(n__head(X)) → head#(activate(X)) | U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) |
| activate#(n__splitAt(X1, X2)) → activate#(X1) | splitAt#(0, XS) → U71#(isLNat(XS), XS) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| activate#(n__splitAt(X1, X2)) → activate#(X2) | U71#(tt, XS) → activate#(XS) |
| U101#(tt, N, XS) → activate#(N) | U81#(tt, N, X, XS) → activate#(XS) |
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| sel#(N, XS) → isNatural#(N) | U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) |
| U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isNatural#(n__s(V1)) → isNatural#(activate(V1)) | take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| U51#(tt, N, XS) → activate#(N) | head#(cons(N, XS)) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U91#(tt, XS) → activate#(XS) |
| U81#(tt, N, X, XS) → activate#(N) | activate#(n__isNatural(X)) → isNatural#(X) |
| activate#(n__isLNat(X)) → isLNat#(X) | U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__s(X)) → activate#(X) | activate#(n__fst(X)) → fst#(activate(X)) |
| isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) |
| U51#(tt, N, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) → activate#(V1) |
| natsFrom#(N) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) |
| fst#(pair(X, Y)) → isLNat#(X) | sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| U41#(tt, N) → cons#(activate(N), n__natsFrom(n__s(activate(N)))) | isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isLNat#(n__tail(V1)) → isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) |
| take#(N, XS) → isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) → activate#(V2) |
| head#(cons(N, XS)) → isNatural#(N) | isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__take(X1, X2)) → activate#(X1) | isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) |
| U11#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) | splitAt#(s(N), cons(X, XS)) → activate#(XS) |
| splitAt#(s(N), cons(X, XS)) → isNatural#(N) | U41#(tt, N) → activate#(N) |
| activate#(n__sel(X1, X2)) → activate#(X1) | U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) |
| activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) | activate#(n__snd(X)) → snd#(activate(X)) |
| activate#(n__snd(X)) → activate#(X) | sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| activate#(n__cons(X1, X2)) → activate#(X1) | U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) |
| tail#(cons(N, XS)) → isNatural#(N) | isLNat#(n__take(V1, V2)) → activate#(V2) |
| tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| activate#(n__tail(X)) → tail#(activate(X)) | activate#(n__natsFrom(X)) → activate#(X) |
| snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U81#(tt, N, X, XS) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) |
| activate#(n__pair(X1, X2)) → activate#(X1) | U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) |
| U82#(pair(YS, ZS), X) → activate#(X) | activate#(n__and(X1, X2)) → activate#(X1) |
| afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| tail#(cons(N, XS)) → activate#(XS) | natsFrom#(N) → U41#(isNatural(N), N) |
| U21#(tt, X) → activate#(X) | isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) |
| U61#(tt, Y) → activate#(Y) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| activate#(n__afterNth(X1, X2)) → activate#(X2) | U101#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V1) | 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)) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U31#(tt, N) → activate#(N) | activate#(n__head(X)) → head#(activate(X)) |
| U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| splitAt#(0, XS) → U71#(isLNat(XS), XS) | isLNat#(n__cons(V1, V2)) → activate#(V1) |
| isNatural#(n__head(V1)) → isLNat#(activate(V1)) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| U71#(tt, XS) → activate#(XS) | U101#(tt, N, XS) → activate#(N) |
| U81#(tt, N, X, XS) → activate#(XS) |
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | activate#(n__tail(X)) | → | activate#(X) | |
| afterNth#(N, XS) | → | isNatural#(N) | U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | |
| splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) | → | activate#(V1) | |
| U82#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | |
| U51#(tt, N, XS) | → | activate#(N) | take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| head#(cons(N, XS)) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | isLNat#(n__tail(V1)) | → | activate#(V1) | |
| U91#(tt, XS) | → | activate#(XS) | activate#(n__isNatural(X)) | → | isNatural#(X) | |
| U81#(tt, N, X, XS) | → | activate#(N) | activate#(n__isLNat(X)) | → | isLNat#(X) | |
| U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| activate#(n__s(X)) | → | activate#(X) | isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | U51#(tt, N, XS) | → | activate#(XS) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | isNatural#(n__s(V1)) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | |
| take#(N, XS) | → | isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | |
| U11#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | U41#(tt, N) | → | activate#(N) | |
| activate#(n__sel(X1, X2)) | → | activate#(X1) | U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| activate#(n__snd(X)) | → | activate#(X) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__pair(X1, X2)) | → | activate#(X2) | U81#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | U82#(pair(YS, ZS), X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| natsFrom#(N) | → | U41#(isNatural(N), N) | tail#(cons(N, XS)) | → | activate#(XS) | |
| U21#(tt, X) | → | activate#(X) | U61#(tt, Y) | → | activate#(Y) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | isNatural#(n__sel(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | U101#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | 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) | |
| U11#(tt, N, XS) | → | activate#(N) | activate#(n__take(X1, X2)) | → | activate#(X2) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U31#(tt, N) | → | activate#(N) | activate#(n__head(X)) | → | head#(activate(X)) | |
| U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | activate#(n__splitAt(X1, X2)) | → | activate#(X2) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| U71#(tt, XS) | → | activate#(XS) | U101#(tt, N, XS) | → | activate#(N) | |
| U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, isNatural, natsFrom, n__snd, n__head, n__sel, n__fst, n__splitAt, fst, activate, n__s, U61, n__0, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, n__natsFrom, tail, splitAt, U71, and, n__cons, n__and, 0, U51, s, tt, U82, take, U81, isLNat, U11, n__pair, afterNth, U31, sel, nil, U101
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| sel#(N, XS) → isNatural#(N) | U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) |
| U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isNatural#(n__s(V1)) → isNatural#(activate(V1)) | take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| U51#(tt, N, XS) → activate#(N) | head#(cons(N, XS)) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U91#(tt, XS) → activate#(XS) |
| U81#(tt, N, X, XS) → activate#(N) | activate#(n__isNatural(X)) → isNatural#(X) |
| activate#(n__isLNat(X)) → isLNat#(X) | U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__s(X)) → activate#(X) | activate#(n__fst(X)) → fst#(activate(X)) |
| isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) |
| U51#(tt, N, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) → activate#(V1) |
| splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) → isNatural#(N) |
| fst#(pair(X, Y)) → isLNat#(X) | sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| head#(cons(N, XS)) → isNatural#(N) | isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | activate#(n__take(X1, X2)) → activate#(X1) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → activate#(V1) |
| isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) | snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) |
| splitAt#(s(N), cons(X, XS)) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → activate#(XS) |
| U41#(tt, N) → activate#(N) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| activate#(n__snd(X)) → snd#(activate(X)) | activate#(n__snd(X)) → activate#(X) |
| sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | activate#(n__cons(X1, X2)) → activate#(X1) |
| U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__take(V1, V2)) → activate#(V2) | tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| isNatural#(n__sel(V1, V2)) → activate#(V2) | activate#(n__tail(X)) → tail#(activate(X)) |
| activate#(n__natsFrom(X)) → activate#(X) | snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) |
| head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) → activate#(X2) |
| U81#(tt, N, X, XS) → activate#(X) | tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) |
| isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | activate#(n__pair(X1, X2)) → activate#(X1) |
| U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) | U82#(pair(YS, ZS), X) → activate#(X) |
| activate#(n__and(X1, X2)) → activate#(X1) | afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| activate#(n__natsFrom(X)) → natsFrom#(activate(X)) | natsFrom#(N) → U41#(isNatural(N), N) |
| tail#(cons(N, XS)) → activate#(XS) | U21#(tt, X) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U61#(tt, Y) → activate#(Y) |
| isNatural#(n__sel(V1, V2)) → activate#(V1) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| U101#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| 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)) |
| isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) |
| isPLNat#(n__pair(V1, V2)) → activate#(V2) | U31#(tt, N) → activate#(N) |
| activate#(n__head(X)) → head#(activate(X)) | U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) |
| activate#(n__splitAt(X1, X2)) → activate#(X1) | splitAt#(0, XS) → U71#(isLNat(XS), XS) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| activate#(n__splitAt(X1, X2)) → activate#(X2) | U71#(tt, XS) → activate#(XS) |
| U101#(tt, N, XS) → activate#(N) | U81#(tt, N, X, XS) → activate#(XS) |
| U11#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | and#(tt, X) | → | activate#(X) | |
| U81#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | |
| activate#(n__head(X)) | → | activate#(X) | activate#(n__tail(X)) | → | activate#(X) | |
| afterNth#(N, XS) | → | isNatural#(N) | U11#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | |
| splitAt#(s(N), cons(X, XS)) | → | and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) | take#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| fst#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) | → | activate#(V1) | |
| U82#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | |
| U51#(tt, N, XS) | → | activate#(N) | take#(N, XS) | → | U101#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| head#(cons(N, XS)) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| isLNat#(n__take(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | fst#(pair(X, Y)) | → | U21#(and(isLNat(X), n__isLNat(Y)), X) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | isLNat#(n__tail(V1)) | → | activate#(V1) | |
| U91#(tt, XS) | → | activate#(XS) | activate#(n__isNatural(X)) | → | isNatural#(X) | |
| U81#(tt, N, X, XS) | → | activate#(N) | activate#(n__isLNat(X)) | → | isLNat#(X) | |
| U101#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| U82#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | activate#(n__s(X)) | → | activate#(X) | |
| isPLNat#(n__splitAt(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) | → | U31#(and(isNatural(N), n__isLNat(activate(XS))), N) | |
| U51#(tt, N, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| afterNth#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| splitAt#(s(N), cons(X, XS)) | → | U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) | → | isNatural#(N) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | sel#(N, XS) | → | U51#(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__cons(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__afterNth(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__sel(V1, V2)) | → | and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | snd#(pair(X, Y)) | → | U61#(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| U41#(tt, N) | → | activate#(N) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | sel#(N, XS) | → | and#(isNatural(N), n__isLNat(XS)) | |
| U51#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | tail#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| activate#(n__natsFrom(X)) | → | activate#(X) | snd#(pair(X, Y)) | → | and#(isLNat(X), n__isLNat(Y)) | |
| head#(cons(N, XS)) | → | and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U81#(tt, N, X, XS) | → | activate#(X) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| isPLNat#(n__pair(V1, V2)) | → | and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | tail#(cons(N, XS)) | → | U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | |
| U82#(pair(YS, ZS), X) | → | activate#(X) | U81#(tt, N, X, XS) | → | U82#(splitAt(activate(N), activate(XS)), activate(X)) | |
| afterNth#(N, XS) | → | U11#(and(isNatural(N), n__isLNat(XS)), N, XS) | activate#(n__and(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | natsFrom#(N) | → | U41#(isNatural(N), N) | |
| tail#(cons(N, XS)) | → | activate#(XS) | U21#(tt, X) | → | activate#(X) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | U61#(tt, Y) | → | activate#(Y) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | activate#(n__afterNth(X1, X2)) | → | activate#(X2) | |
| U101#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| 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)) | |
| isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | U31#(tt, N) | → | activate#(N) | |
| activate#(n__head(X)) | → | head#(activate(X)) | U51#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X1) | splitAt#(0, XS) | → | U71#(isLNat(XS), XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | U71#(tt, XS) | → | activate#(XS) | |
| U101#(tt, N, XS) | → | activate#(N) | U81#(tt, N, X, XS) | → | activate#(XS) |
| U101(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | U11(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | |
| U21(tt, X) | → | activate(X) | U31(tt, N) | → | activate(N) | |
| U41(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U51(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | |
| U61(tt, Y) | → | activate(Y) | U71(tt, XS) | → | pair(nil, activate(XS)) | |
| U81(tt, N, X, XS) | → | U82(splitAt(activate(N), activate(XS)), activate(X)) | U82(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U91(tt, XS) | → | activate(XS) | afterNth(N, XS) | → | U11(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| and(tt, X) | → | activate(X) | fst(pair(X, Y)) | → | U21(and(isLNat(X), n__isLNat(Y)), X) | |
| head(cons(N, XS)) | → | U31(and(isNatural(N), n__isLNat(activate(XS))), N) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat(n__cons(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | |
| isLNat(n__fst(V1)) | → | isPLNat(activate(V1)) | isLNat(n__natsFrom(V1)) | → | isNatural(activate(V1)) | |
| isLNat(n__snd(V1)) | → | isPLNat(activate(V1)) | isLNat(n__tail(V1)) | → | isLNat(activate(V1)) | |
| isLNat(n__take(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | isLNat(activate(V1)) | isNatural(n__s(V1)) | → | isNatural(activate(V1)) | |
| isNatural(n__sel(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | isPLNat(n__pair(V1, V2)) | → | and(isLNat(activate(V1)), n__isLNat(activate(V2))) | |
| isPLNat(n__splitAt(V1, V2)) | → | and(isNatural(activate(V1)), n__isLNat(activate(V2))) | natsFrom(N) | → | U41(isNatural(N), N) | |
| sel(N, XS) | → | U51(and(isNatural(N), n__isLNat(XS)), N, XS) | snd(pair(X, Y)) | → | U61(and(isLNat(X), n__isLNat(Y)), Y) | |
| splitAt(0, XS) | → | U71(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) | take(N, XS) | → | U101(and(isNatural(N), n__isLNat(XS)), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(X) | |
| isLNat(X) | → | n__isLNat(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) | and(X1, X2) | → | n__and(X1, X2) | |
| isNatural(X) | → | n__isNatural(X) | activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | |
| activate(n__s(X)) | → | s(activate(X)) | activate(n__isLNat(X)) | → | isLNat(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__and(X1, X2)) | → | and(activate(X1), X2) | activate(n__isNatural(X)) | → | isNatural(X) | |
| activate(X) | → | X |
Termination of terms over the following signature is verified: pair, isNatural, natsFrom, n__snd, n__head, n__sel, n__fst, n__splitAt, fst, activate, n__s, U61, n__0, n__afterNth, n__isLNat, U41, U91, n__isNatural, n__nil, head, U21, cons, snd, n__tail, isPLNat, n__take, n__natsFrom, tail, splitAt, U71, and, n__cons, n__and, 0, U51, s, tt, U82, take, U81, isLNat, U11, n__pair, afterNth, U31, sel, nil, U101
| U11#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | and#(tt, X) → activate#(X) |
| sel#(N, XS) → isNatural#(N) | U81#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) |
| isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → and#(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) |
| U11#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) | take#(N, XS) → and#(isNatural(N), n__isLNat(XS)) |
| fst#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) | isLNat#(n__cons(V1, V2)) → activate#(V2) |
| isLNat#(n__take(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__take(V1, V2)) → activate#(V1) |
| isNatural#(n__s(V1)) → isNatural#(activate(V1)) | take#(N, XS) → U101#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| U51#(tt, N, XS) → activate#(N) | head#(cons(N, XS)) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | isLNat#(n__take(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| fst#(pair(X, Y)) → U21#(and(isLNat(X), n__isLNat(Y)), X) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U91#(tt, XS) → activate#(XS) |
| U81#(tt, N, X, XS) → activate#(N) | activate#(n__isNatural(X)) → isNatural#(X) |
| activate#(n__isLNat(X)) → isLNat#(X) | U101#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__s(X)) → activate#(X) | activate#(n__fst(X)) → fst#(activate(X)) |
| isPLNat#(n__splitAt(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | head#(cons(N, XS)) → U31#(and(isNatural(N), n__isLNat(activate(XS))), N) |
| U51#(tt, N, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| afterNth#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | isNatural#(n__head(V1)) → activate#(V1) |
| splitAt#(s(N), cons(X, XS)) → U81#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) | natsFrom#(N) → isNatural#(N) |
| fst#(pair(X, Y)) → isLNat#(X) | sel#(N, XS) → U51#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__cons(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | isLNat#(n__afterNth(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| head#(cons(N, XS)) → isNatural#(N) | isNatural#(n__sel(V1, V2)) → and#(isNatural(activate(V1)), n__isLNat(activate(V2))) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | activate#(n__take(X1, X2)) → activate#(X1) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → activate#(V1) |
| isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) | snd#(pair(X, Y)) → U61#(and(isLNat(X), n__isLNat(Y)), Y) |
| splitAt#(s(N), cons(X, XS)) → isNatural#(N) | splitAt#(s(N), cons(X, XS)) → activate#(XS) |
| U41#(tt, N) → activate#(N) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| activate#(n__snd(X)) → snd#(activate(X)) | activate#(n__snd(X)) → activate#(X) |
| sel#(N, XS) → and#(isNatural(N), n__isLNat(XS)) | activate#(n__cons(X1, X2)) → activate#(X1) |
| U51#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | tail#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__take(V1, V2)) → activate#(V2) | tail#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) |
| isNatural#(n__sel(V1, V2)) → activate#(V2) | activate#(n__tail(X)) → tail#(activate(X)) |
| activate#(n__natsFrom(X)) → activate#(X) | snd#(pair(X, Y)) → and#(isLNat(X), n__isLNat(Y)) |
| head#(cons(N, XS)) → and#(isNatural(N), n__isLNat(activate(XS))) | activate#(n__pair(X1, X2)) → activate#(X2) |
| U81#(tt, N, X, XS) → activate#(X) | tail#(cons(N, XS)) → U91#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) |
| isPLNat#(n__pair(V1, V2)) → and#(isLNat(activate(V1)), n__isLNat(activate(V2))) | activate#(n__pair(X1, X2)) → activate#(X1) |
| U81#(tt, N, X, XS) → U82#(splitAt(activate(N), activate(XS)), activate(X)) | U82#(pair(YS, ZS), X) → activate#(X) |
| activate#(n__and(X1, X2)) → activate#(X1) | afterNth#(N, XS) → U11#(and(isNatural(N), n__isLNat(XS)), N, XS) |
| activate#(n__natsFrom(X)) → natsFrom#(activate(X)) | natsFrom#(N) → U41#(isNatural(N), N) |
| tail#(cons(N, XS)) → activate#(XS) | U21#(tt, X) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U61#(tt, Y) → activate#(Y) |
| isNatural#(n__sel(V1, V2)) → activate#(V1) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| U101#(tt, N, XS) → activate#(XS) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| 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)) |
| isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) |
| isPLNat#(n__pair(V1, V2)) → activate#(V2) | U31#(tt, N) → activate#(N) |
| activate#(n__head(X)) → head#(activate(X)) | U51#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) |
| activate#(n__splitAt(X1, X2)) → activate#(X1) | splitAt#(0, XS) → U71#(isLNat(XS), XS) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| activate#(n__splitAt(X1, X2)) → activate#(X2) | U71#(tt, XS) → activate#(XS) |
| U101#(tt, N, XS) → activate#(N) | U81#(tt, N, X, XS) → activate#(XS) |