The TRS could not be proven terminating. The proof attempt took 60016 ms.
Problem 1 was processed with processor DependencyGraph (45312ms). | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (14624ms)]. | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (timeout)]. | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (2ms)]. | – Problem 5 remains open; application of the following processors failed [SubtermCriterion (2ms)]. | – Problem 6 remains open; application of the following processors failed [SubtermCriterion (2ms)]. | – Problem 7 remains open; application of the following processors failed [SubtermCriterion (3ms)].
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | |
| sel#(N, XS) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| U171#(tt, N, XS) | → | isLNat#(activate(XS)) | snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | |
| U221#(tt, N, XS) | → | isLNat#(activate(XS)) | U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | |
| U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | U51#(tt, V2) | → | activate#(V2) | |
| 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)) | |
| head#(cons(N, XS)) | → | activate#(XS) | U31#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U201#(tt, N, X, XS) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | U181#(tt, Y) | → | activate#(Y) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U172#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, N, X, XS) | → | activate#(N) | U202#(tt, N, X, XS) | → | activate#(N) | |
| U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | |
| U141#(tt, V2) | → | isLNat#(activate(V2)) | splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | |
| U211#(tt, XS) | → | isLNat#(activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | activate#(n__s(X)) | → | activate#(X) | |
| splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| U212#(tt, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| U221#(tt, N, XS) | → | activate#(XS) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| natsFrom#(N) | → | U161#(isNatural(N), N) | U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) | → | activate#(X) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| U203#(tt, N, X, XS) | → | activate#(X) | U211#(tt, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | U181#(tt, Y) | → | isLNat#(activate(Y)) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | U201#(tt, N, X, XS) | → | activate#(N) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | U22#(tt, X) | → | activate#(X) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| U204#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | U51#(tt, V2) | → | isLNat#(activate(V2)) | |
| U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | U101#(tt, V2) | → | isLNat#(activate(V2)) | |
| U131#(tt, V2) | → | activate#(V2) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| sel#(N, XS) | → | U171#(isNatural(N), N, XS) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| U172#(tt, N, XS) | → | activate#(XS) | U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| U171#(tt, N, XS) | → | activate#(XS) | U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U31#(tt, N, XS) | → | activate#(N) | U191#(tt, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| U131#(tt, V2) | → | isLNat#(activate(V2)) | isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | |
| U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U21#(tt, X, Y) | → | activate#(Y) | U221#(tt, N, XS) | → | activate#(N) | |
| U12#(tt, N, XS) | → | activate#(N) | U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U41#(tt, V2) | → | isLNat#(activate(V2)) | U182#(tt, Y) | → | activate#(Y) | |
| U203#(tt, N, X, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U202#(tt, N, X, XS) | → | activate#(XS) | U222#(tt, N, XS) | → | activate#(N) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| U21#(tt, X, Y) | → | activate#(X) | tail#(cons(N, XS)) | → | activate#(XS) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | U31#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| U11#(tt, N, XS) | → | isLNat#(activate(XS)) | U41#(tt, V2) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| U201#(tt, N, X, XS) | → | activate#(X) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | |
| 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) | |
| U202#(tt, N, X, XS) | → | activate#(X) | activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | |
| U171#(tt, N, XS) | → | activate#(N) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | U32#(tt, N) | → | activate#(N) | |
| U101#(tt, V2) | → | activate#(V2) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) | → | activate#(V2) | |
| U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | U151#(tt, V2) | → | isLNat#(activate(V2)) | |
| U151#(tt, V2) | → | activate#(V2) | isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | isLNat#(activate(Y)) | U12#(tt, N, XS) | → | activate#(XS) | |
| U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | take#(N, XS) | → | U221#(isNatural(N), N, XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U41#(tt, V2) | → | U42#(isLNat(activate(V2))) | |
| U222#(tt, N, XS) | → | activate#(XS) | fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | |
| isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, isPLNat, U152, tail, n__natsFrom, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, n__pair, U12, afterNth, U102, sel, U101, nil
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| U171#(tt, N, XS) | → | isLNat#(activate(XS)) | snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | |
| U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | U221#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | U51#(tt, V2) | → | activate#(V2) | |
| 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)) | |
| head#(cons(N, XS)) | → | activate#(XS) | U31#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | U201#(tt, N, X, XS) | → | activate#(XS) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | U181#(tt, Y) | → | activate#(Y) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U172#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, N, X, XS) | → | activate#(N) | U202#(tt, N, X, XS) | → | activate#(N) | |
| U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | |
| U141#(tt, V2) | → | isLNat#(activate(V2)) | splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | |
| U211#(tt, XS) | → | isLNat#(activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | activate#(n__s(X)) | → | activate#(X) | |
| splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| U212#(tt, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| U221#(tt, N, XS) | → | activate#(XS) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| natsFrom#(N) | → | U161#(isNatural(N), N) | natsFrom#(N) | → | isNatural#(N) | |
| U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) | → | activate#(X) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| U211#(tt, XS) | → | activate#(XS) | U203#(tt, N, X, XS) | → | activate#(X) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | U181#(tt, Y) | → | isLNat#(activate(Y)) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | U201#(tt, N, X, XS) | → | activate#(N) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | U22#(tt, X) | → | activate#(X) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| U204#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | U51#(tt, V2) | → | isLNat#(activate(V2)) | |
| U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, V2) | → | isLNat#(activate(V2)) | U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | |
| U131#(tt, V2) | → | activate#(V2) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| sel#(N, XS) | → | U171#(isNatural(N), N, XS) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| U172#(tt, N, XS) | → | activate#(XS) | U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| U171#(tt, N, XS) | → | activate#(XS) | U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U31#(tt, N, XS) | → | activate#(N) | U191#(tt, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| U131#(tt, V2) | → | isLNat#(activate(V2)) | isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | |
| U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U21#(tt, X, Y) | → | activate#(Y) | U221#(tt, N, XS) | → | activate#(N) | |
| U12#(tt, N, XS) | → | activate#(N) | U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U41#(tt, V2) | → | isLNat#(activate(V2)) | U182#(tt, Y) | → | activate#(Y) | |
| U203#(tt, N, X, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U202#(tt, N, X, XS) | → | activate#(XS) | U222#(tt, N, XS) | → | activate#(N) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| tail#(cons(N, XS)) | → | activate#(XS) | U21#(tt, X, Y) | → | activate#(X) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | U31#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| U11#(tt, N, XS) | → | isLNat#(activate(XS)) | U41#(tt, V2) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| U201#(tt, N, X, XS) | → | activate#(X) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | |
| 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) | |
| U202#(tt, N, X, XS) | → | activate#(X) | activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | |
| U171#(tt, N, XS) | → | activate#(N) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | U32#(tt, N) | → | activate#(N) | |
| U101#(tt, V2) | → | activate#(V2) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) | → | activate#(V2) | |
| U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | |
| U151#(tt, V2) | → | isLNat#(activate(V2)) | U151#(tt, V2) | → | activate#(V2) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | isLNat#(activate(Y)) | U12#(tt, N, XS) | → | activate#(XS) | |
| U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | take#(N, XS) | → | U221#(isNatural(N), N, XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U222#(tt, N, XS) | → | activate#(XS) | |
| fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, isPLNat, U152, tail, n__natsFrom, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, n__pair, U12, afterNth, U102, sel, U101, nil
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | |
| sel#(N, XS) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| U171#(tt, N, XS) | → | isLNat#(activate(XS)) | snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | |
| U221#(tt, N, XS) | → | isLNat#(activate(XS)) | U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | |
| U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | U51#(tt, V2) | → | activate#(V2) | |
| 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)) | |
| head#(cons(N, XS)) | → | activate#(XS) | U31#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| snd#(pair(X, Y)) | → | isLNat#(X) | U201#(tt, N, X, XS) | → | activate#(XS) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | U181#(tt, Y) | → | activate#(Y) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U172#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, N, X, XS) | → | activate#(N) | U202#(tt, N, X, XS) | → | activate#(N) | |
| U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | |
| U141#(tt, V2) | → | isLNat#(activate(V2)) | splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | |
| U211#(tt, XS) | → | isLNat#(activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | activate#(n__s(X)) | → | activate#(X) | |
| splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| U212#(tt, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| U221#(tt, N, XS) | → | activate#(XS) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| natsFrom#(N) | → | U161#(isNatural(N), N) | U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) | → | activate#(X) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| U203#(tt, N, X, XS) | → | activate#(X) | U211#(tt, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | U181#(tt, Y) | → | isLNat#(activate(Y)) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | U201#(tt, N, X, XS) | → | activate#(N) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | U22#(tt, X) | → | activate#(X) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| U204#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | U51#(tt, V2) | → | isLNat#(activate(V2)) | |
| U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | U101#(tt, V2) | → | isLNat#(activate(V2)) | |
| U131#(tt, V2) | → | activate#(V2) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| sel#(N, XS) | → | U171#(isNatural(N), N, XS) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| U172#(tt, N, XS) | → | activate#(XS) | U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| U171#(tt, N, XS) | → | activate#(XS) | U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U31#(tt, N, XS) | → | activate#(N) | U191#(tt, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| U131#(tt, V2) | → | isLNat#(activate(V2)) | U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | |
| isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U21#(tt, X, Y) | → | activate#(Y) | U221#(tt, N, XS) | → | activate#(N) | |
| U12#(tt, N, XS) | → | activate#(N) | U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U41#(tt, V2) | → | isLNat#(activate(V2)) | U182#(tt, Y) | → | activate#(Y) | |
| U203#(tt, N, X, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U202#(tt, N, X, XS) | → | activate#(XS) | U222#(tt, N, XS) | → | activate#(N) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| U21#(tt, X, Y) | → | activate#(X) | tail#(cons(N, XS)) | → | activate#(XS) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | U31#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| U11#(tt, N, XS) | → | isLNat#(activate(XS)) | U41#(tt, V2) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| U201#(tt, N, X, XS) | → | activate#(X) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | U151#(tt, V2) | → | U152#(isLNat(activate(V2))) | |
| tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | 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) | U202#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | U171#(tt, N, XS) | → | activate#(N) | |
| isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| U32#(tt, N) | → | activate#(N) | U101#(tt, V2) | → | activate#(V2) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | |
| U141#(tt, V2) | → | activate#(V2) | U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | U151#(tt, V2) | → | activate#(V2) | |
| U151#(tt, V2) | → | isLNat#(activate(V2)) | activate#(n__head(X)) | → | head#(activate(X)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X1) | U21#(tt, X, Y) | → | isLNat#(activate(Y)) | |
| U12#(tt, N, XS) | → | activate#(XS) | U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| take#(N, XS) | → | U221#(isNatural(N), N, XS) | activate#(n__splitAt(X1, X2)) | → | activate#(X2) | |
| U222#(tt, N, XS) | → | activate#(XS) | fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | |
| isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, isPLNat, U152, tail, n__natsFrom, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, n__pair, U12, afterNth, U102, sel, U101, nil
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | |
| sel#(N, XS) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | |
| U171#(tt, N, XS) | → | isLNat#(activate(XS)) | snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | |
| U221#(tt, N, XS) | → | isLNat#(activate(XS)) | U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | |
| U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | U51#(tt, V2) | → | activate#(V2) | |
| 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)) | |
| head#(cons(N, XS)) | → | activate#(XS) | U31#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U201#(tt, N, X, XS) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | U181#(tt, Y) | → | activate#(Y) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U172#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, N, X, XS) | → | activate#(N) | U202#(tt, N, X, XS) | → | activate#(N) | |
| U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | |
| U141#(tt, V2) | → | isLNat#(activate(V2)) | splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | |
| U211#(tt, XS) | → | isLNat#(activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | activate#(n__s(X)) | → | activate#(X) | |
| splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | activate#(n__fst(X)) | → | fst#(activate(X)) | |
| U212#(tt, XS) | → | activate#(XS) | isLNat#(n__natsFrom(V1)) | → | activate#(V1) | |
| U221#(tt, N, XS) | → | activate#(XS) | isNatural#(n__head(V1)) | → | activate#(V1) | |
| natsFrom#(N) | → | U161#(isNatural(N), N) | U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| natsFrom#(N) | → | isNatural#(N) | fst#(pair(X, Y)) | → | isLNat#(X) | |
| isNatural#(n__s(V1)) | → | activate#(V1) | isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | |
| isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) | → | activate#(X) | |
| isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | take#(N, XS) | → | isNatural#(N) | |
| U203#(tt, N, X, XS) | → | activate#(X) | U211#(tt, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | head#(cons(N, XS)) | → | isNatural#(N) | |
| isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | U181#(tt, Y) | → | isLNat#(activate(Y)) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | U201#(tt, N, X, XS) | → | activate#(N) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U11#(tt, N, XS) | → | activate#(XS) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | U22#(tt, X) | → | activate#(X) | |
| isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | isLNat#(n__snd(V1)) | → | activate#(V1) | |
| U204#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | U51#(tt, V2) | → | isLNat#(activate(V2)) | |
| U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, V2) | → | isLNat#(activate(V2)) | U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | |
| U131#(tt, V2) | → | activate#(V2) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| U51#(tt, V2) | → | U52#(isLNat(activate(V2))) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| activate#(n__snd(X)) | → | activate#(X) | U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | |
| U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | sel#(N, XS) | → | U171#(isNatural(N), N, XS) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | U172#(tt, N, XS) | → | activate#(XS) | |
| U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V2) | U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U171#(tt, N, XS) | → | activate#(XS) | U31#(tt, N, XS) | → | activate#(N) | |
| U191#(tt, XS) | → | activate#(XS) | isNatural#(n__sel(V1, V2)) | → | activate#(V2) | |
| activate#(n__tail(X)) | → | tail#(activate(X)) | U131#(tt, V2) | → | isLNat#(activate(V2)) | |
| isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | |
| activate#(n__natsFrom(X)) | → | activate#(X) | U161#(tt, N) | → | activate#(N) | |
| U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | U21#(tt, X, Y) | → | activate#(Y) | |
| U221#(tt, N, XS) | → | activate#(N) | U12#(tt, N, XS) | → | activate#(N) | |
| U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | U41#(tt, V2) | → | isLNat#(activate(V2)) | |
| U182#(tt, Y) | → | activate#(Y) | U203#(tt, N, X, XS) | → | activate#(XS) | |
| activate#(n__pair(X1, X2)) | → | activate#(X2) | U202#(tt, N, X, XS) | → | activate#(XS) | |
| U222#(tt, N, XS) | → | activate#(N) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | U21#(tt, X, Y) | → | activate#(X) | |
| tail#(cons(N, XS)) | → | activate#(XS) | isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | |
| U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | |
| U31#(tt, N, XS) | → | activate#(XS) | isNatural#(n__sel(V1, V2)) | → | activate#(V1) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | U11#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U41#(tt, V2) | → | activate#(V2) | head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | |
| isLNat#(n__fst(V1)) | → | activate#(V1) | U201#(tt, N, X, XS) | → | activate#(X) | |
| splitAt#(0, XS) | → | isLNat#(XS) | activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | |
| tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | 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) | U202#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | U171#(tt, N, XS) | → | activate#(N) | |
| isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| U32#(tt, N) | → | activate#(N) | U101#(tt, V2) | → | activate#(V2) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | |
| U141#(tt, V2) | → | activate#(V2) | U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | U151#(tt, V2) | → | isLNat#(activate(V2)) | |
| U151#(tt, V2) | → | activate#(V2) | activate#(n__head(X)) | → | head#(activate(X)) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X1) | U21#(tt, X, Y) | → | isLNat#(activate(Y)) | |
| U12#(tt, N, XS) | → | activate#(XS) | U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V1) | isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | |
| take#(N, XS) | → | U221#(isNatural(N), N, XS) | activate#(n__splitAt(X1, X2)) | → | activate#(X2) | |
| U222#(tt, N, XS) | → | activate#(XS) | fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | |
| isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, isPLNat, U152, tail, n__natsFrom, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, n__pair, U12, afterNth, U102, sel, U101, nil
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | sel#(N, XS) | → | isNatural#(N) | |
| U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U191#(tt, XS) | → | pair#(nil, activate(XS)) | |
| U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | U171#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | |
| U221#(tt, N, XS) | → | isLNat#(activate(XS)) | U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | |
| U51#(tt, V2) | → | activate#(V2) | 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)) | head#(cons(N, XS)) | → | activate#(XS) | |
| U31#(tt, N, XS) | → | isLNat#(activate(XS)) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| U201#(tt, N, X, XS) | → | activate#(XS) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| U181#(tt, Y) | → | activate#(Y) | isLNat#(n__tail(V1)) | → | activate#(V1) | |
| U172#(tt, N, XS) | → | activate#(N) | U203#(tt, N, X, XS) | → | activate#(N) | |
| U202#(tt, N, X, XS) | → | activate#(N) | U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | |
| isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | U141#(tt, V2) | → | isLNat#(activate(V2)) | |
| splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | U211#(tt, XS) | → | isLNat#(activate(XS)) | |
| activate#(n__fst(X)) | → | activate#(X) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| activate#(n__s(X)) | → | activate#(X) | splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | U212#(tt, XS) | → | activate#(XS) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | U221#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | natsFrom#(N) | → | U161#(isNatural(N), N) | |
| U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | natsFrom#(N) | → | isNatural#(N) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | isNatural#(n__s(V1)) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| U204#(pair(YS, ZS), X) | → | activate#(X) | isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | |
| take#(N, XS) | → | isNatural#(N) | U211#(tt, XS) | → | activate#(XS) | |
| U203#(tt, N, X, XS) | → | activate#(X) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | |
| U181#(tt, Y) | → | isLNat#(activate(Y)) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| U201#(tt, N, X, XS) | → | activate#(N) | isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | |
| U11#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | |
| U22#(tt, X) | → | activate#(X) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | U204#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | |
| U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | |
| U51#(tt, V2) | → | isLNat#(activate(V2)) | U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | |
| activate#(n__sel(X1, X2)) | → | activate#(X1) | U101#(tt, V2) | → | isLNat#(activate(V2)) | |
| U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | U131#(tt, V2) | → | activate#(V2) | |
| activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| activate#(n__snd(X)) | → | activate#(X) | U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | sel#(N, XS) | → | U171#(isNatural(N), N, XS) | |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | U172#(tt, N, XS) | → | activate#(XS) | |
| U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| U191#(tt, XS) | → | nil# | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| U171#(tt, N, XS) | → | activate#(XS) | U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U31#(tt, N, XS) | → | activate#(N) | U191#(tt, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| U131#(tt, V2) | → | isLNat#(activate(V2)) | isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | |
| U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U21#(tt, X, Y) | → | activate#(Y) | U221#(tt, N, XS) | → | activate#(N) | |
| U12#(tt, N, XS) | → | activate#(N) | U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U41#(tt, V2) | → | isLNat#(activate(V2)) | U182#(tt, Y) | → | activate#(Y) | |
| U203#(tt, N, X, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U202#(tt, N, X, XS) | → | activate#(XS) | U222#(tt, N, XS) | → | activate#(N) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| tail#(cons(N, XS)) | → | activate#(XS) | U21#(tt, X, Y) | → | activate#(X) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | U31#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| U11#(tt, N, XS) | → | isLNat#(activate(XS)) | U41#(tt, V2) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| U201#(tt, N, X, XS) | → | activate#(X) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | |
| 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) | |
| U202#(tt, N, X, XS) | → | activate#(X) | activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | |
| U171#(tt, N, XS) | → | activate#(N) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | U32#(tt, N) | → | activate#(N) | |
| U101#(tt, V2) | → | activate#(V2) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) | → | activate#(V2) | |
| U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | U151#(tt, V2) | → | isLNat#(activate(V2)) | |
| U151#(tt, V2) | → | activate#(V2) | isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | isLNat#(activate(Y)) | U12#(tt, N, XS) | → | activate#(XS) | |
| U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | take#(N, XS) | → | U221#(isNatural(N), N, XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U222#(tt, N, XS) | → | activate#(XS) | |
| fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, isPLNat, U152, tail, n__natsFrom, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, n__pair, U12, afterNth, U102, sel, U101, nil
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | |
| sel#(N, XS) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| activate#(n__head(X)) | → | activate#(X) | afterNth#(N, XS) | → | isNatural#(N) | |
| activate#(n__tail(X)) | → | activate#(X) | U191#(tt, XS) | → | pair#(nil, activate(XS)) | |
| U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | U171#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | U221#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | |
| U51#(tt, V2) | → | activate#(V2) | 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)) | head#(cons(N, XS)) | → | activate#(XS) | |
| U31#(tt, N, XS) | → | isLNat#(activate(XS)) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| U201#(tt, N, X, XS) | → | activate#(XS) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| U181#(tt, Y) | → | activate#(Y) | isLNat#(n__tail(V1)) | → | activate#(V1) | |
| U172#(tt, N, XS) | → | activate#(N) | U203#(tt, N, X, XS) | → | activate#(N) | |
| U202#(tt, N, X, XS) | → | activate#(N) | U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | |
| isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | U141#(tt, V2) | → | isLNat#(activate(V2)) | |
| splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | U211#(tt, XS) | → | isLNat#(activate(XS)) | |
| activate#(n__fst(X)) | → | activate#(X) | activate#(n__sel(X1, X2)) | → | activate#(X2) | |
| activate#(n__s(X)) | → | activate#(X) | splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | U212#(tt, XS) | → | activate#(XS) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | U221#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | natsFrom#(N) | → | U161#(isNatural(N), N) | |
| natsFrom#(N) | → | isNatural#(N) | U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | isNatural#(n__s(V1)) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| U204#(pair(YS, ZS), X) | → | activate#(X) | isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | |
| take#(N, XS) | → | isNatural#(N) | U211#(tt, XS) | → | activate#(XS) | |
| U203#(tt, N, X, XS) | → | activate#(X) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | |
| U181#(tt, Y) | → | isLNat#(activate(Y)) | activate#(n__take(X1, X2)) | → | activate#(X1) | |
| U201#(tt, N, X, XS) | → | activate#(N) | isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | |
| U11#(tt, N, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | |
| U22#(tt, X) | → | activate#(X) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | |
| splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | |
| afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | U51#(tt, V2) | → | isLNat#(activate(V2)) | |
| U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | U101#(tt, V2) | → | isLNat#(activate(V2)) | |
| U131#(tt, V2) | → | activate#(V2) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| activate#(n__snd(X)) | → | snd#(activate(X)) | activate#(n__snd(X)) | → | activate#(X) | |
| U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| sel#(N, XS) | → | U171#(isNatural(N), N, XS) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| U172#(tt, N, XS) | → | activate#(XS) | U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| tail#(cons(N, XS)) | → | isNatural#(N) | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | U171#(tt, N, XS) | → | activate#(XS) | |
| U31#(tt, N, XS) | → | activate#(N) | U191#(tt, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| U131#(tt, V2) | → | isLNat#(activate(V2)) | isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | |
| U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U21#(tt, X, Y) | → | activate#(Y) | U221#(tt, N, XS) | → | activate#(N) | |
| U12#(tt, N, XS) | → | activate#(N) | U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U41#(tt, V2) | → | isLNat#(activate(V2)) | U182#(tt, Y) | → | activate#(Y) | |
| U203#(tt, N, X, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U202#(tt, N, X, XS) | → | activate#(XS) | U222#(tt, N, XS) | → | activate#(N) | |
| activate#(n__pair(X1, X2)) | → | activate#(X1) | activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | |
| tail#(cons(N, XS)) | → | activate#(XS) | U21#(tt, X, Y) | → | activate#(X) | |
| isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | U31#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V1) | isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | |
| activate#(n__afterNth(X1, X2)) | → | activate#(X2) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | |
| U11#(tt, N, XS) | → | isLNat#(activate(XS)) | U41#(tt, V2) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | isLNat#(n__fst(V1)) | → | activate#(V1) | |
| U201#(tt, N, X, XS) | → | activate#(X) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | |
| 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) | |
| U202#(tt, N, X, XS) | → | activate#(X) | activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | |
| U171#(tt, N, XS) | → | activate#(N) | isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | |
| activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | U32#(tt, N) | → | activate#(N) | |
| U101#(tt, V2) | → | activate#(V2) | isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | |
| U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) | → | activate#(V2) | |
| U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | |
| U151#(tt, V2) | → | isLNat#(activate(V2)) | U151#(tt, V2) | → | activate#(V2) | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | isLNat#(activate(Y)) | U12#(tt, N, XS) | → | activate#(XS) | |
| U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | take#(N, XS) | → | U221#(isNatural(N), N, XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U222#(tt, N, XS) | → | activate#(XS) | |
| fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, isPLNat, U152, tail, n__natsFrom, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U142, U202, U141, s, U51, tt, take, U81, U52, U11, n__pair, U12, afterNth, U102, sel, U101, nil
| U171#(tt, N, XS) | → | U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) | → | U204#(splitAt(activate(N), activate(XS)), activate(X)) | |
| sel#(N, XS) | → | isNatural#(N) | isLNat#(n__afterNth(V1, V2)) | → | isNatural#(activate(V1)) | |
| isLNat#(n__fst(V1)) | → | U61#(isPLNat(activate(V1))) | activate#(n__head(X)) | → | activate#(X) | |
| afterNth#(N, XS) | → | isNatural#(N) | activate#(n__tail(X)) | → | activate#(X) | |
| U204#(pair(YS, ZS), X) | → | pair#(cons(activate(X), YS), ZS) | U191#(tt, XS) | → | pair#(nil, activate(XS)) | |
| U171#(tt, N, XS) | → | isLNat#(activate(XS)) | activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) | |
| snd#(pair(X, Y)) | → | U181#(isLNat(X), Y) | U221#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U31#(tt, N, XS) | → | U32#(isLNat(activate(XS)), activate(N)) | isLNat#(n__tail(V1)) | → | U91#(isLNat(activate(V1))) | |
| U202#(tt, N, X, XS) | → | isLNat#(activate(XS)) | U51#(tt, V2) | → | activate#(V2) | |
| isLNat#(n__cons(V1, V2)) | → | activate#(V2) | U161#(tt, N) | → | cons#(activate(N), n__natsFrom(n__s(activate(N)))) | |
| isLNat#(n__take(V1, V2)) | → | activate#(V1) | isLNat#(n__take(V1, V2)) | → | isNatural#(activate(V1)) | |
| isNatural#(n__s(V1)) | → | isNatural#(activate(V1)) | U141#(tt, V2) | → | U142#(isLNat(activate(V2))) | |
| head#(cons(N, XS)) | → | activate#(XS) | U31#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| U201#(tt, N, X, XS) | → | activate#(XS) | snd#(pair(X, Y)) | → | isLNat#(X) | |
| U181#(tt, Y) | → | activate#(Y) | isPLNat#(n__pair(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__tail(V1)) | → | activate#(V1) | U172#(tt, N, XS) | → | activate#(N) | |
| U203#(tt, N, X, XS) | → | activate#(N) | U202#(tt, N, X, XS) | → | activate#(N) | |
| U101#(tt, V2) | → | U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) | → | U141#(isLNat(activate(V1)), activate(V2)) | |
| U141#(tt, V2) | → | isLNat#(activate(V2)) | splitAt#(0, XS) | → | U191#(isLNat(XS), XS) | |
| U211#(tt, XS) | → | isLNat#(activate(XS)) | activate#(n__fst(X)) | → | activate#(X) | |
| activate#(n__sel(X1, X2)) | → | activate#(X2) | isNatural#(n__head(V1)) | → | U111#(isLNat(activate(V1))) | |
| splitAt#(s(N), cons(X, XS)) | → | U201#(isNatural(N), N, X, activate(XS)) | activate#(n__s(X)) | → | activate#(X) | |
| activate#(n__fst(X)) | → | fst#(activate(X)) | U212#(tt, XS) | → | activate#(XS) | |
| isLNat#(n__natsFrom(V1)) | → | activate#(V1) | U221#(tt, N, XS) | → | activate#(XS) | |
| isNatural#(n__head(V1)) | → | activate#(V1) | natsFrom#(N) | → | U161#(isNatural(N), N) | |
| natsFrom#(N) | → | isNatural#(N) | U172#(tt, N, XS) | → | afterNth#(activate(N), activate(XS)) | |
| fst#(pair(X, Y)) | → | isLNat#(X) | isNatural#(n__s(V1)) | → | activate#(V1) | |
| isLNat#(n__afterNth(V1, V2)) | → | activate#(V2) | isLNat#(n__tail(V1)) | → | isLNat#(activate(V1)) | |
| U204#(pair(YS, ZS), X) | → | activate#(X) | isLNat#(n__cons(V1, V2)) | → | isNatural#(activate(V1)) | |
| take#(N, XS) | → | isNatural#(N) | U203#(tt, N, X, XS) | → | activate#(X) | |
| U211#(tt, XS) | → | activate#(XS) | isPLNat#(n__splitAt(V1, V2)) | → | activate#(V2) | |
| head#(cons(N, XS)) | → | isNatural#(N) | isNatural#(n__sel(V1, V2)) | → | isNatural#(activate(V1)) | |
| U181#(tt, Y) | → | isLNat#(activate(Y)) | isLNat#(n__natsFrom(V1)) | → | U71#(isNatural(activate(V1))) | |
| activate#(n__take(X1, X2)) | → | activate#(X1) | U201#(tt, N, X, XS) | → | activate#(N) | |
| isLNat#(n__natsFrom(V1)) | → | isNatural#(activate(V1)) | U131#(tt, V2) | → | U132#(isLNat(activate(V2))) | |
| U11#(tt, N, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | pair#(activate(X1), activate(X2)) | |
| isPLNat#(n__splitAt(V1, V2)) | → | isNatural#(activate(V1)) | isLNat#(n__snd(V1)) | → | U81#(isPLNat(activate(V1))) | |
| U22#(tt, X) | → | activate#(X) | activate#(n__s(X)) | → | s#(activate(X)) | |
| isLNat#(n__snd(V1)) | → | activate#(V1) | isLNat#(n__snd(V1)) | → | isPLNat#(activate(V1)) | |
| U204#(pair(YS, ZS), X) | → | cons#(activate(X), YS) | U181#(tt, Y) | → | U182#(isLNat(activate(Y)), activate(Y)) | |
| splitAt#(s(N), cons(X, XS)) | → | activate#(XS) | splitAt#(s(N), cons(X, XS)) | → | isNatural#(N) | |
| afterNth#(N, XS) | → | U11#(isNatural(N), N, XS) | U51#(tt, V2) | → | isLNat#(activate(V2)) | |
| U211#(tt, XS) | → | U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) | → | activate#(X1) | |
| U101#(tt, V2) | → | isLNat#(activate(V2)) | U21#(tt, X, Y) | → | U22#(isLNat(activate(Y)), activate(X)) | |
| U131#(tt, V2) | → | activate#(V2) | activate#(n__take(X1, X2)) | → | take#(activate(X1), activate(X2)) | |
| U51#(tt, V2) | → | U52#(isLNat(activate(V2))) | activate#(n__snd(X)) | → | snd#(activate(X)) | |
| activate#(n__snd(X)) | → | activate#(X) | activate#(n__cons(X1, X2)) | → | activate#(X1) | |
| sel#(N, XS) | → | U171#(isNatural(N), N, XS) | U201#(tt, N, X, XS) | → | U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | |
| U12#(tt, N, XS) | → | snd#(splitAt(activate(N), activate(XS))) | U172#(tt, N, XS) | → | head#(afterNth(activate(N), activate(XS))) | |
| U172#(tt, N, XS) | → | activate#(XS) | tail#(cons(N, XS)) | → | isNatural#(N) | |
| U191#(tt, XS) | → | nil# | isLNat#(n__take(V1, V2)) | → | activate#(V2) | |
| U171#(tt, N, XS) | → | activate#(XS) | U203#(tt, N, X, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U31#(tt, N, XS) | → | activate#(N) | U191#(tt, XS) | → | activate#(XS) | |
| isNatural#(n__sel(V1, V2)) | → | activate#(V2) | activate#(n__tail(X)) | → | tail#(activate(X)) | |
| U131#(tt, V2) | → | isLNat#(activate(V2)) | U201#(tt, N, X, XS) | → | isNatural#(activate(X)) | |
| isPLNat#(n__splitAt(V1, V2)) | → | U151#(isNatural(activate(V1)), activate(V2)) | activate#(n__natsFrom(X)) | → | activate#(X) | |
| U161#(tt, N) | → | activate#(N) | U221#(tt, N, XS) | → | activate#(N) | |
| U21#(tt, X, Y) | → | activate#(Y) | U11#(tt, N, XS) | → | U12#(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U12#(tt, N, XS) | → | activate#(N) | U222#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | |
| U41#(tt, V2) | → | isLNat#(activate(V2)) | U182#(tt, Y) | → | activate#(Y) | |
| U203#(tt, N, X, XS) | → | activate#(XS) | activate#(n__pair(X1, X2)) | → | activate#(X2) | |
| U202#(tt, N, X, XS) | → | activate#(XS) | activate#(n__0) | → | 0# | |
| U222#(tt, N, XS) | → | activate#(N) | activate#(n__pair(X1, X2)) | → | activate#(X1) | |
| activate#(n__natsFrom(X)) | → | natsFrom#(activate(X)) | U21#(tt, X, Y) | → | activate#(X) | |
| tail#(cons(N, XS)) | → | activate#(XS) | isPLNat#(n__pair(V1, V2)) | → | isLNat#(activate(V1)) | |
| U221#(tt, N, XS) | → | U222#(isLNat(activate(XS)), activate(N), activate(XS)) | isNatural#(n__sel(V1, V2)) | → | U131#(isNatural(activate(V1)), activate(V2)) | |
| U31#(tt, N, XS) | → | activate#(XS) | isNatural#(n__sel(V1, V2)) | → | activate#(V1) | |
| isLNat#(n__cons(V1, V2)) | → | U51#(isNatural(activate(V1)), activate(V2)) | activate#(n__afterNth(X1, X2)) | → | activate#(X2) | |
| isPLNat#(n__splitAt(V1, V2)) | → | activate#(V1) | U11#(tt, N, XS) | → | isLNat#(activate(XS)) | |
| head#(cons(N, XS)) | → | U31#(isNatural(N), N, activate(XS)) | U41#(tt, V2) | → | activate#(V2) | |
| isLNat#(n__fst(V1)) | → | activate#(V1) | isNatural#(n__s(V1)) | → | U121#(isNatural(activate(V1))) | |
| U201#(tt, N, X, XS) | → | activate#(X) | splitAt#(0, XS) | → | isLNat#(XS) | |
| activate#(n__splitAt(X1, X2)) | → | splitAt#(activate(X1), activate(X2)) | U151#(tt, V2) | → | U152#(isLNat(activate(V2))) | |
| tail#(cons(N, XS)) | → | U211#(isNatural(N), activate(XS)) | 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) | U202#(tt, N, X, XS) | → | activate#(X) | |
| activate#(n__afterNth(X1, X2)) | → | afterNth#(activate(X1), activate(X2)) | U171#(tt, N, XS) | → | activate#(N) | |
| isLNat#(n__fst(V1)) | → | isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) | → | sel#(activate(X1), activate(X2)) | |
| U32#(tt, N) | → | activate#(N) | U101#(tt, V2) | → | activate#(V2) | |
| isPLNat#(n__pair(V1, V2)) | → | activate#(V2) | U222#(tt, N, XS) | → | fst#(splitAt(activate(N), activate(XS))) | |
| U141#(tt, V2) | → | activate#(V2) | U202#(tt, N, X, XS) | → | U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| isLNat#(n__afterNth(V1, V2)) | → | U41#(isNatural(activate(V1)), activate(V2)) | U151#(tt, V2) | → | activate#(V2) | |
| U151#(tt, V2) | → | isLNat#(activate(V2)) | activate#(n__nil) | → | nil# | |
| activate#(n__head(X)) | → | head#(activate(X)) | activate#(n__splitAt(X1, X2)) | → | activate#(X1) | |
| U21#(tt, X, Y) | → | isLNat#(activate(Y)) | U12#(tt, N, XS) | → | activate#(XS) | |
| U12#(tt, N, XS) | → | splitAt#(activate(N), activate(XS)) | isLNat#(n__cons(V1, V2)) | → | activate#(V1) | |
| isNatural#(n__head(V1)) | → | isLNat#(activate(V1)) | take#(N, XS) | → | U221#(isNatural(N), N, XS) | |
| activate#(n__splitAt(X1, X2)) | → | activate#(X2) | U41#(tt, V2) | → | U42#(isLNat(activate(V2))) | |
| U222#(tt, N, XS) | → | activate#(XS) | fst#(pair(X, Y)) | → | U21#(isLNat(X), X, Y) | |
| isLNat#(n__take(V1, V2)) | → | U101#(isNatural(activate(V1)), activate(V2)) |
| U101(tt, V2) | → | U102(isLNat(activate(V2))) | U102(tt) | → | tt | |
| U11(tt, N, XS) | → | U12(isLNat(activate(XS)), activate(N), activate(XS)) | U111(tt) | → | tt | |
| U12(tt, N, XS) | → | snd(splitAt(activate(N), activate(XS))) | U121(tt) | → | tt | |
| U131(tt, V2) | → | U132(isLNat(activate(V2))) | U132(tt) | → | tt | |
| U141(tt, V2) | → | U142(isLNat(activate(V2))) | U142(tt) | → | tt | |
| U151(tt, V2) | → | U152(isLNat(activate(V2))) | U152(tt) | → | tt | |
| U161(tt, N) | → | cons(activate(N), n__natsFrom(n__s(activate(N)))) | U171(tt, N, XS) | → | U172(isLNat(activate(XS)), activate(N), activate(XS)) | |
| U172(tt, N, XS) | → | head(afterNth(activate(N), activate(XS))) | U181(tt, Y) | → | U182(isLNat(activate(Y)), activate(Y)) | |
| U182(tt, Y) | → | activate(Y) | U191(tt, XS) | → | pair(nil, activate(XS)) | |
| U201(tt, N, X, XS) | → | U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U202(tt, N, X, XS) | → | U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | |
| U203(tt, N, X, XS) | → | U204(splitAt(activate(N), activate(XS)), activate(X)) | U204(pair(YS, ZS), X) | → | pair(cons(activate(X), YS), ZS) | |
| U21(tt, X, Y) | → | U22(isLNat(activate(Y)), activate(X)) | U211(tt, XS) | → | U212(isLNat(activate(XS)), activate(XS)) | |
| U212(tt, XS) | → | activate(XS) | U22(tt, X) | → | activate(X) | |
| U221(tt, N, XS) | → | U222(isLNat(activate(XS)), activate(N), activate(XS)) | U222(tt, N, XS) | → | fst(splitAt(activate(N), activate(XS))) | |
| U31(tt, N, XS) | → | U32(isLNat(activate(XS)), activate(N)) | U32(tt, N) | → | activate(N) | |
| U41(tt, V2) | → | U42(isLNat(activate(V2))) | U42(tt) | → | tt | |
| U51(tt, V2) | → | U52(isLNat(activate(V2))) | U52(tt) | → | tt | |
| U61(tt) | → | tt | U71(tt) | → | tt | |
| U81(tt) | → | tt | U91(tt) | → | tt | |
| afterNth(N, XS) | → | U11(isNatural(N), N, XS) | fst(pair(X, Y)) | → | U21(isLNat(X), X, Y) | |
| head(cons(N, XS)) | → | U31(isNatural(N), N, activate(XS)) | isLNat(n__nil) | → | tt | |
| isLNat(n__afterNth(V1, V2)) | → | U41(isNatural(activate(V1)), activate(V2)) | isLNat(n__cons(V1, V2)) | → | U51(isNatural(activate(V1)), activate(V2)) | |
| isLNat(n__fst(V1)) | → | U61(isPLNat(activate(V1))) | isLNat(n__natsFrom(V1)) | → | U71(isNatural(activate(V1))) | |
| isLNat(n__snd(V1)) | → | U81(isPLNat(activate(V1))) | isLNat(n__tail(V1)) | → | U91(isLNat(activate(V1))) | |
| isLNat(n__take(V1, V2)) | → | U101(isNatural(activate(V1)), activate(V2)) | isNatural(n__0) | → | tt | |
| isNatural(n__head(V1)) | → | U111(isLNat(activate(V1))) | isNatural(n__s(V1)) | → | U121(isNatural(activate(V1))) | |
| isNatural(n__sel(V1, V2)) | → | U131(isNatural(activate(V1)), activate(V2)) | isPLNat(n__pair(V1, V2)) | → | U141(isLNat(activate(V1)), activate(V2)) | |
| isPLNat(n__splitAt(V1, V2)) | → | U151(isNatural(activate(V1)), activate(V2)) | natsFrom(N) | → | U161(isNatural(N), N) | |
| sel(N, XS) | → | U171(isNatural(N), N, XS) | snd(pair(X, Y)) | → | U181(isLNat(X), Y) | |
| splitAt(0, XS) | → | U191(isLNat(XS), XS) | splitAt(s(N), cons(X, XS)) | → | U201(isNatural(N), N, X, activate(XS)) | |
| tail(cons(N, XS)) | → | U211(isNatural(N), activate(XS)) | take(N, XS) | → | U221(isNatural(N), N, XS) | |
| natsFrom(X) | → | n__natsFrom(X) | s(X) | → | n__s(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) | |
| activate(n__natsFrom(X)) | → | natsFrom(activate(X)) | activate(n__s(X)) | → | s(activate(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(X) | → | X |
Termination of terms over the following signature is verified: natsFrom, U161, U204, n__snd, U203, n__sel, n__fst, n__s, activate, fst, U111, U61, U211, U212, n__nil, head, U21, U22, n__tail, U151, U152, isPLNat, n__natsFrom, tail, U71, U191, n__cons, 0, U121, U221, isLNat, U222, U31, U32, U181, U182, pair, isNatural, n__head, n__splitAt, U132, n__0, U131, n__afterNth, U42, U41, U91, cons, snd, U171, U172, n__take, splitAt, U201, U202, U142, U141, U51, s, tt, take, U52, U81, U11, U12, n__pair, afterNth, U102, sel, nil, U101
| U171#(tt, N, XS) → U172#(isLNat(activate(XS)), activate(N), activate(XS)) | sel#(N, XS) → isNatural#(N) |
| U203#(tt, N, X, XS) → U204#(splitAt(activate(N), activate(XS)), activate(X)) | isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U204#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) |
| U191#(tt, XS) → pair#(nil, activate(XS)) | U171#(tt, N, XS) → isLNat#(activate(XS)) |
| snd#(pair(X, Y)) → U181#(isLNat(X), Y) | U31#(tt, N, XS) → U32#(isLNat(activate(XS)), activate(N)) |
| U221#(tt, N, XS) → isLNat#(activate(XS)) | U202#(tt, N, X, XS) → isLNat#(activate(XS)) |
| U51#(tt, V2) → activate#(V2) | 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)) | head#(cons(N, XS)) → activate#(XS) |
| U201#(tt, N, X, XS) → activate#(XS) | snd#(pair(X, Y)) → isLNat#(X) |
| U31#(tt, N, XS) → isLNat#(activate(XS)) | U181#(tt, Y) → activate#(Y) |
| isPLNat#(n__pair(V1, V2)) → activate#(V1) | isLNat#(n__tail(V1)) → activate#(V1) |
| U172#(tt, N, XS) → activate#(N) | U203#(tt, N, X, XS) → activate#(N) |
| U202#(tt, N, X, XS) → activate#(N) | U101#(tt, V2) → U102#(isLNat(activate(V2))) |
| isPLNat#(n__pair(V1, V2)) → U141#(isLNat(activate(V1)), activate(V2)) | U141#(tt, V2) → isLNat#(activate(V2)) |
| splitAt#(0, XS) → U191#(isLNat(XS), XS) | U211#(tt, XS) → isLNat#(activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__fst(X)) → fst#(activate(X)) | splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, activate(XS)) |
| activate#(n__s(X)) → activate#(X) | U212#(tt, XS) → activate#(XS) |
| isLNat#(n__natsFrom(V1)) → activate#(V1) | U221#(tt, N, XS) → activate#(XS) |
| isNatural#(n__head(V1)) → activate#(V1) | natsFrom#(N) → U161#(isNatural(N), N) |
| U172#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | natsFrom#(N) → isNatural#(N) |
| fst#(pair(X, Y)) → isLNat#(X) | isNatural#(n__s(V1)) → activate#(V1) |
| isLNat#(n__afterNth(V1, V2)) → activate#(V2) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| U204#(pair(YS, ZS), X) → activate#(X) | isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) |
| take#(N, XS) → isNatural#(N) | U203#(tt, N, X, XS) → activate#(X) |
| U211#(tt, XS) → activate#(XS) | head#(cons(N, XS)) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) |
| U181#(tt, Y) → isLNat#(activate(Y)) | activate#(n__take(X1, X2)) → activate#(X1) |
| U201#(tt, N, X, XS) → activate#(N) | isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) |
| U11#(tt, N, XS) → activate#(XS) | U22#(tt, X) → activate#(X) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → activate#(V1) |
| isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) | U181#(tt, Y) → U182#(isLNat(activate(Y)), activate(Y)) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| afterNth#(N, XS) → U11#(isNatural(N), N, XS) | U51#(tt, V2) → isLNat#(activate(V2)) |
| U211#(tt, XS) → U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, V2) → isLNat#(activate(V2)) | U21#(tt, X, Y) → U22#(isLNat(activate(Y)), activate(X)) |
| U131#(tt, V2) → activate#(V2) | 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) → U171#(isNatural(N), N, XS) |
| U201#(tt, N, X, XS) → U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U12#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| U172#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | U172#(tt, N, XS) → activate#(XS) |
| tail#(cons(N, XS)) → isNatural#(N) | isLNat#(n__take(V1, V2)) → activate#(V2) |
| U171#(tt, N, XS) → activate#(XS) | U203#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) |
| U31#(tt, N, XS) → activate#(N) | U191#(tt, XS) → activate#(XS) |
| activate#(n__tail(X)) → tail#(activate(X)) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| U131#(tt, V2) → isLNat#(activate(V2)) | activate#(n__natsFrom(X)) → activate#(X) |
| U201#(tt, N, X, XS) → isNatural#(activate(X)) | isPLNat#(n__splitAt(V1, V2)) → U151#(isNatural(activate(V1)), activate(V2)) |
| U161#(tt, N) → activate#(N) | U221#(tt, N, XS) → activate#(N) |
| U21#(tt, X, Y) → activate#(Y) | U11#(tt, N, XS) → U12#(isLNat(activate(XS)), activate(N), activate(XS)) |
| U12#(tt, N, XS) → activate#(N) | U222#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| U41#(tt, V2) → isLNat#(activate(V2)) | U182#(tt, Y) → activate#(Y) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U203#(tt, N, X, XS) → activate#(XS) |
| U202#(tt, N, X, XS) → activate#(XS) | U222#(tt, N, XS) → activate#(N) |
| activate#(n__pair(X1, X2)) → activate#(X1) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| U21#(tt, X, Y) → activate#(X) | tail#(cons(N, XS)) → activate#(XS) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U221#(tt, N, XS) → U222#(isLNat(activate(XS)), activate(N), activate(XS)) |
| isNatural#(n__sel(V1, V2)) → U131#(isNatural(activate(V1)), activate(V2)) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| U31#(tt, N, XS) → activate#(XS) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| isLNat#(n__cons(V1, V2)) → U51#(isNatural(activate(V1)), activate(V2)) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| U11#(tt, N, XS) → isLNat#(activate(XS)) | head#(cons(N, XS)) → U31#(isNatural(N), N, activate(XS)) |
| U41#(tt, V2) → activate#(V2) | isLNat#(n__fst(V1)) → activate#(V1) |
| U201#(tt, N, X, XS) → activate#(X) | splitAt#(0, XS) → isLNat#(XS) |
| activate#(n__splitAt(X1, X2)) → splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) → U211#(isNatural(N), activate(XS)) |
| 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)) | U202#(tt, N, X, XS) → activate#(X) |
| U171#(tt, N, XS) → activate#(N) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | U32#(tt, N) → activate#(N) |
| U101#(tt, V2) → activate#(V2) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U222#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) → activate#(V2) |
| U202#(tt, N, X, XS) → U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | activate#(n__head(X)) → head#(activate(X)) |
| U151#(tt, V2) → activate#(V2) | U151#(tt, V2) → isLNat#(activate(V2)) |
| isLNat#(n__afterNth(V1, V2)) → U41#(isNatural(activate(V1)), activate(V2)) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| U21#(tt, X, Y) → isLNat#(activate(Y)) | U12#(tt, N, XS) → activate#(XS) |
| U12#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| take#(N, XS) → U221#(isNatural(N), N, XS) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | U222#(tt, N, XS) → activate#(XS) |
| isLNat#(n__take(V1, V2)) → U101#(isNatural(activate(V1)), activate(V2)) | fst#(pair(X, Y)) → U21#(isLNat(X), X, Y) |
| U171#(tt, N, XS) → U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) → U204#(splitAt(activate(N), activate(XS)), activate(X)) |
| sel#(N, XS) → isNatural#(N) | isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U204#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) |
| U191#(tt, XS) → pair#(nil, activate(XS)) | U171#(tt, N, XS) → isLNat#(activate(XS)) |
| snd#(pair(X, Y)) → U181#(isLNat(X), Y) | U221#(tt, N, XS) → isLNat#(activate(XS)) |
| U31#(tt, N, XS) → U32#(isLNat(activate(XS)), activate(N)) | U202#(tt, N, X, XS) → isLNat#(activate(XS)) |
| U51#(tt, V2) → activate#(V2) | 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)) | head#(cons(N, XS)) → activate#(XS) |
| U201#(tt, N, X, XS) → activate#(XS) | snd#(pair(X, Y)) → isLNat#(X) |
| U31#(tt, N, XS) → isLNat#(activate(XS)) | U181#(tt, Y) → activate#(Y) |
| isPLNat#(n__pair(V1, V2)) → activate#(V1) | isLNat#(n__tail(V1)) → activate#(V1) |
| U172#(tt, N, XS) → activate#(N) | U203#(tt, N, X, XS) → activate#(N) |
| U202#(tt, N, X, XS) → activate#(N) | U101#(tt, V2) → U102#(isLNat(activate(V2))) |
| isPLNat#(n__pair(V1, V2)) → U141#(isLNat(activate(V1)), activate(V2)) | U141#(tt, V2) → isLNat#(activate(V2)) |
| splitAt#(0, XS) → U191#(isLNat(XS), XS) | U211#(tt, XS) → isLNat#(activate(XS)) |
| activate#(n__fst(X)) → activate#(X) | activate#(n__sel(X1, X2)) → activate#(X2) |
| activate#(n__fst(X)) → fst#(activate(X)) | splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, activate(XS)) |
| activate#(n__s(X)) → activate#(X) | U212#(tt, XS) → activate#(XS) |
| isLNat#(n__natsFrom(V1)) → activate#(V1) | U221#(tt, N, XS) → activate#(XS) |
| isNatural#(n__head(V1)) → activate#(V1) | natsFrom#(N) → U161#(isNatural(N), N) |
| natsFrom#(N) → isNatural#(N) | U172#(tt, N, XS) → afterNth#(activate(N), activate(XS)) |
| fst#(pair(X, Y)) → isLNat#(X) | isNatural#(n__s(V1)) → activate#(V1) |
| isLNat#(n__afterNth(V1, V2)) → activate#(V2) | isLNat#(n__tail(V1)) → isLNat#(activate(V1)) |
| U204#(pair(YS, ZS), X) → activate#(X) | isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) |
| take#(N, XS) → isNatural#(N) | U203#(tt, N, X, XS) → activate#(X) |
| U211#(tt, XS) → activate#(XS) | head#(cons(N, XS)) → isNatural#(N) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V2) | isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) |
| U181#(tt, Y) → isLNat#(activate(Y)) | activate#(n__take(X1, X2)) → activate#(X1) |
| U201#(tt, N, X, XS) → activate#(N) | isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) |
| U11#(tt, N, XS) → activate#(XS) | U22#(tt, X) → activate#(X) |
| isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) | isLNat#(n__snd(V1)) → activate#(V1) |
| isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) | U204#(pair(YS, ZS), X) → cons#(activate(X), YS) |
| U181#(tt, Y) → U182#(isLNat(activate(Y)), activate(Y)) | splitAt#(s(N), cons(X, XS)) → activate#(XS) |
| splitAt#(s(N), cons(X, XS)) → isNatural#(N) | afterNth#(N, XS) → U11#(isNatural(N), N, XS) |
| U51#(tt, V2) → isLNat#(activate(V2)) | U211#(tt, XS) → U212#(isLNat(activate(XS)), activate(XS)) |
| activate#(n__sel(X1, X2)) → activate#(X1) | U21#(tt, X, Y) → U22#(isLNat(activate(Y)), activate(X)) |
| U101#(tt, V2) → isLNat#(activate(V2)) | U131#(tt, V2) → activate#(V2) |
| 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) → U171#(isNatural(N), N, XS) | U12#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| U201#(tt, N, X, XS) → U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U172#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) |
| U172#(tt, N, XS) → activate#(XS) | tail#(cons(N, XS)) → isNatural#(N) |
| U191#(tt, XS) → nil# | isLNat#(n__take(V1, V2)) → activate#(V2) |
| U203#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | U171#(tt, N, XS) → activate#(XS) |
| U31#(tt, N, XS) → activate#(N) | U191#(tt, XS) → activate#(XS) |
| activate#(n__tail(X)) → tail#(activate(X)) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| U131#(tt, V2) → isLNat#(activate(V2)) | activate#(n__natsFrom(X)) → activate#(X) |
| U201#(tt, N, X, XS) → isNatural#(activate(X)) | isPLNat#(n__splitAt(V1, V2)) → U151#(isNatural(activate(V1)), activate(V2)) |
| U161#(tt, N) → activate#(N) | U221#(tt, N, XS) → activate#(N) |
| U21#(tt, X, Y) → activate#(Y) | U11#(tt, N, XS) → U12#(isLNat(activate(XS)), activate(N), activate(XS)) |
| U12#(tt, N, XS) → activate#(N) | U222#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| U41#(tt, V2) → isLNat#(activate(V2)) | U182#(tt, Y) → activate#(Y) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U203#(tt, N, X, XS) → activate#(XS) |
| U202#(tt, N, X, XS) → activate#(XS) | U222#(tt, N, XS) → activate#(N) |
| activate#(n__pair(X1, X2)) → activate#(X1) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| U21#(tt, X, Y) → activate#(X) | tail#(cons(N, XS)) → activate#(XS) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U221#(tt, N, XS) → U222#(isLNat(activate(XS)), activate(N), activate(XS)) |
| isNatural#(n__sel(V1, V2)) → U131#(isNatural(activate(V1)), activate(V2)) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| U31#(tt, N, XS) → activate#(XS) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| isLNat#(n__cons(V1, V2)) → U51#(isNatural(activate(V1)), activate(V2)) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| U11#(tt, N, XS) → isLNat#(activate(XS)) | head#(cons(N, XS)) → U31#(isNatural(N), N, activate(XS)) |
| U41#(tt, V2) → activate#(V2) | isLNat#(n__fst(V1)) → activate#(V1) |
| U201#(tt, N, X, XS) → activate#(X) | splitAt#(0, XS) → isLNat#(XS) |
| activate#(n__splitAt(X1, X2)) → splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) → U211#(isNatural(N), activate(XS)) |
| 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)) | U202#(tt, N, X, XS) → activate#(X) |
| U171#(tt, N, XS) → activate#(N) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | U32#(tt, N) → activate#(N) |
| U101#(tt, V2) → activate#(V2) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U222#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) → activate#(V2) |
| U202#(tt, N, X, XS) → U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | activate#(n__head(X)) → head#(activate(X)) |
| isLNat#(n__afterNth(V1, V2)) → U41#(isNatural(activate(V1)), activate(V2)) | U151#(tt, V2) → activate#(V2) |
| U151#(tt, V2) → isLNat#(activate(V2)) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| U21#(tt, X, Y) → isLNat#(activate(Y)) | U12#(tt, N, XS) → activate#(XS) |
| U12#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| take#(N, XS) → U221#(isNatural(N), N, XS) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | U222#(tt, N, XS) → activate#(XS) |
| isLNat#(n__take(V1, V2)) → U101#(isNatural(activate(V1)), activate(V2)) | fst#(pair(X, Y)) → U21#(isLNat(X), X, Y) |
| U171#(tt, N, XS) → U172#(isLNat(activate(XS)), activate(N), activate(XS)) | U203#(tt, N, X, XS) → U204#(splitAt(activate(N), activate(XS)), activate(X)) |
| sel#(N, XS) → isNatural#(N) | isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U204#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) |
| U171#(tt, N, XS) → isLNat#(activate(XS)) | snd#(pair(X, Y)) → U181#(isLNat(X), Y) |
| U221#(tt, N, XS) → isLNat#(activate(XS)) | U31#(tt, N, XS) → U32#(isLNat(activate(XS)), activate(N)) |
| U202#(tt, N, X, XS) → isLNat#(activate(XS)) | U51#(tt, V2) → activate#(V2) |
| 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)) |
| head#(cons(N, XS)) → activate#(XS) | U201#(tt, N, X, XS) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | U31#(tt, N, XS) → isLNat#(activate(XS)) |
| U181#(tt, Y) → activate#(Y) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U172#(tt, N, XS) → activate#(N) |
| U203#(tt, N, X, XS) → activate#(N) | U202#(tt, N, X, XS) → activate#(N) |
| U101#(tt, V2) → U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) → U141#(isLNat(activate(V1)), activate(V2)) |
| U141#(tt, V2) → isLNat#(activate(V2)) | splitAt#(0, XS) → U191#(isLNat(XS), XS) |
| U211#(tt, XS) → isLNat#(activate(XS)) | activate#(n__fst(X)) → activate#(X) |
| activate#(n__sel(X1, X2)) → activate#(X2) | activate#(n__fst(X)) → fst#(activate(X)) |
| splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, activate(XS)) | activate#(n__s(X)) → activate#(X) |
| U212#(tt, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| U221#(tt, N, XS) → activate#(XS) | isNatural#(n__head(V1)) → activate#(V1) |
| natsFrom#(N) → U161#(isNatural(N), N) | U172#(tt, N, XS) → afterNth#(activate(N), activate(XS)) |
| natsFrom#(N) → isNatural#(N) | fst#(pair(X, Y)) → isLNat#(X) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__tail(V1)) → isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) → activate#(X) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| U203#(tt, N, X, XS) → activate#(X) | U211#(tt, XS) → activate#(XS) |
| head#(cons(N, XS)) → isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) → activate#(V2) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | U181#(tt, Y) → isLNat#(activate(Y)) |
| activate#(n__take(X1, X2)) → activate#(X1) | U201#(tt, N, X, XS) → activate#(N) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| U22#(tt, X) → activate#(X) | isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| U204#(pair(YS, ZS), X) → cons#(activate(X), YS) | U181#(tt, Y) → U182#(isLNat(activate(Y)), activate(Y)) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| afterNth#(N, XS) → U11#(isNatural(N), N, XS) | U51#(tt, V2) → isLNat#(activate(V2)) |
| U211#(tt, XS) → U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U21#(tt, X, Y) → U22#(isLNat(activate(Y)), activate(X)) | U101#(tt, V2) → isLNat#(activate(V2)) |
| U131#(tt, V2) → activate#(V2) | 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) → U171#(isNatural(N), N, XS) |
| U201#(tt, N, X, XS) → U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U12#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| U172#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | U172#(tt, N, XS) → activate#(XS) |
| tail#(cons(N, XS)) → isNatural#(N) | isLNat#(n__take(V1, V2)) → activate#(V2) |
| U203#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | U171#(tt, N, XS) → activate#(XS) |
| U31#(tt, N, XS) → activate#(N) | U191#(tt, XS) → activate#(XS) |
| activate#(n__tail(X)) → tail#(activate(X)) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| U131#(tt, V2) → isLNat#(activate(V2)) | activate#(n__natsFrom(X)) → activate#(X) |
| U201#(tt, N, X, XS) → isNatural#(activate(X)) | isPLNat#(n__splitAt(V1, V2)) → U151#(isNatural(activate(V1)), activate(V2)) |
| U161#(tt, N) → activate#(N) | U221#(tt, N, XS) → activate#(N) |
| U21#(tt, X, Y) → activate#(Y) | U11#(tt, N, XS) → U12#(isLNat(activate(XS)), activate(N), activate(XS)) |
| U12#(tt, N, XS) → activate#(N) | U222#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| U41#(tt, V2) → isLNat#(activate(V2)) | U182#(tt, Y) → activate#(Y) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U203#(tt, N, X, XS) → activate#(XS) |
| U202#(tt, N, X, XS) → activate#(XS) | U222#(tt, N, XS) → activate#(N) |
| activate#(n__pair(X1, X2)) → activate#(X1) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| U21#(tt, X, Y) → activate#(X) | tail#(cons(N, XS)) → activate#(XS) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U221#(tt, N, XS) → U222#(isLNat(activate(XS)), activate(N), activate(XS)) |
| isNatural#(n__sel(V1, V2)) → U131#(isNatural(activate(V1)), activate(V2)) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| U31#(tt, N, XS) → activate#(XS) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| isLNat#(n__cons(V1, V2)) → U51#(isNatural(activate(V1)), activate(V2)) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| U11#(tt, N, XS) → isLNat#(activate(XS)) | head#(cons(N, XS)) → U31#(isNatural(N), N, activate(XS)) |
| U41#(tt, V2) → activate#(V2) | isLNat#(n__fst(V1)) → activate#(V1) |
| U201#(tt, N, X, XS) → activate#(X) | splitAt#(0, XS) → isLNat#(XS) |
| activate#(n__splitAt(X1, X2)) → splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) → U211#(isNatural(N), activate(XS)) |
| 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)) | U202#(tt, N, X, XS) → activate#(X) |
| U171#(tt, N, XS) → activate#(N) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | U32#(tt, N) → activate#(N) |
| U101#(tt, V2) → activate#(V2) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U222#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) → activate#(V2) |
| U202#(tt, N, X, XS) → U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | activate#(n__head(X)) → head#(activate(X)) |
| U151#(tt, V2) → activate#(V2) | U151#(tt, V2) → isLNat#(activate(V2)) |
| isLNat#(n__afterNth(V1, V2)) → U41#(isNatural(activate(V1)), activate(V2)) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| U21#(tt, X, Y) → isLNat#(activate(Y)) | U12#(tt, N, XS) → activate#(XS) |
| U12#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| take#(N, XS) → U221#(isNatural(N), N, XS) | isLNat#(n__cons(V1, V2)) → activate#(V1) |
| isNatural#(n__head(V1)) → isLNat#(activate(V1)) | U222#(tt, N, XS) → activate#(XS) |
| isLNat#(n__take(V1, V2)) → U101#(isNatural(activate(V1)), activate(V2)) | fst#(pair(X, Y)) → U21#(isLNat(X), X, Y) |
| U171#(tt, N, XS) → U172#(isLNat(activate(XS)), activate(N), activate(XS)) | sel#(N, XS) → isNatural#(N) |
| U203#(tt, N, X, XS) → U204#(splitAt(activate(N), activate(XS)), activate(X)) | isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U204#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) |
| U171#(tt, N, XS) → isLNat#(activate(XS)) | snd#(pair(X, Y)) → U181#(isLNat(X), Y) |
| U31#(tt, N, XS) → U32#(isLNat(activate(XS)), activate(N)) | U221#(tt, N, XS) → isLNat#(activate(XS)) |
| U202#(tt, N, X, XS) → isLNat#(activate(XS)) | U51#(tt, V2) → activate#(V2) |
| 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)) |
| head#(cons(N, XS)) → activate#(XS) | snd#(pair(X, Y)) → isLNat#(X) |
| U201#(tt, N, X, XS) → activate#(XS) | U31#(tt, N, XS) → isLNat#(activate(XS)) |
| U181#(tt, Y) → activate#(Y) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U172#(tt, N, XS) → activate#(N) |
| U203#(tt, N, X, XS) → activate#(N) | U202#(tt, N, X, XS) → activate#(N) |
| U101#(tt, V2) → U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) → U141#(isLNat(activate(V1)), activate(V2)) |
| U141#(tt, V2) → isLNat#(activate(V2)) | splitAt#(0, XS) → U191#(isLNat(XS), XS) |
| U211#(tt, XS) → isLNat#(activate(XS)) | activate#(n__fst(X)) → activate#(X) |
| activate#(n__sel(X1, X2)) → activate#(X2) | activate#(n__fst(X)) → fst#(activate(X)) |
| splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, activate(XS)) | activate#(n__s(X)) → activate#(X) |
| U212#(tt, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| U221#(tt, N, XS) → activate#(XS) | isNatural#(n__head(V1)) → activate#(V1) |
| natsFrom#(N) → U161#(isNatural(N), N) | natsFrom#(N) → isNatural#(N) |
| U172#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | fst#(pair(X, Y)) → isLNat#(X) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__tail(V1)) → isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) → activate#(X) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| U211#(tt, XS) → activate#(XS) | U203#(tt, N, X, XS) → activate#(X) |
| head#(cons(N, XS)) → isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) → activate#(V2) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | U181#(tt, Y) → isLNat#(activate(Y)) |
| activate#(n__take(X1, X2)) → activate#(X1) | U201#(tt, N, X, XS) → activate#(N) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| U22#(tt, X) → activate#(X) | isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| U204#(pair(YS, ZS), X) → cons#(activate(X), YS) | U181#(tt, Y) → U182#(isLNat(activate(Y)), activate(Y)) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| afterNth#(N, XS) → U11#(isNatural(N), N, XS) | U51#(tt, V2) → isLNat#(activate(V2)) |
| U211#(tt, XS) → U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, V2) → isLNat#(activate(V2)) | U21#(tt, X, Y) → U22#(isLNat(activate(Y)), activate(X)) |
| U131#(tt, V2) → activate#(V2) | 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) → U171#(isNatural(N), N, XS) |
| U201#(tt, N, X, XS) → U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U12#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| U172#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | U172#(tt, N, XS) → activate#(XS) |
| tail#(cons(N, XS)) → isNatural#(N) | isLNat#(n__take(V1, V2)) → activate#(V2) |
| U203#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | U171#(tt, N, XS) → activate#(XS) |
| U31#(tt, N, XS) → activate#(N) | U191#(tt, XS) → activate#(XS) |
| activate#(n__tail(X)) → tail#(activate(X)) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| U131#(tt, V2) → isLNat#(activate(V2)) | activate#(n__natsFrom(X)) → activate#(X) |
| U201#(tt, N, X, XS) → isNatural#(activate(X)) | isPLNat#(n__splitAt(V1, V2)) → U151#(isNatural(activate(V1)), activate(V2)) |
| U161#(tt, N) → activate#(N) | U221#(tt, N, XS) → activate#(N) |
| U21#(tt, X, Y) → activate#(Y) | U11#(tt, N, XS) → U12#(isLNat(activate(XS)), activate(N), activate(XS)) |
| U12#(tt, N, XS) → activate#(N) | U222#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| U41#(tt, V2) → isLNat#(activate(V2)) | U182#(tt, Y) → activate#(Y) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U203#(tt, N, X, XS) → activate#(XS) |
| U202#(tt, N, X, XS) → activate#(XS) | U222#(tt, N, XS) → activate#(N) |
| activate#(n__pair(X1, X2)) → activate#(X1) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| tail#(cons(N, XS)) → activate#(XS) | U21#(tt, X, Y) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U221#(tt, N, XS) → U222#(isLNat(activate(XS)), activate(N), activate(XS)) |
| isNatural#(n__sel(V1, V2)) → U131#(isNatural(activate(V1)), activate(V2)) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| U31#(tt, N, XS) → activate#(XS) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| isLNat#(n__cons(V1, V2)) → U51#(isNatural(activate(V1)), activate(V2)) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| U11#(tt, N, XS) → isLNat#(activate(XS)) | head#(cons(N, XS)) → U31#(isNatural(N), N, activate(XS)) |
| U41#(tt, V2) → activate#(V2) | isLNat#(n__fst(V1)) → activate#(V1) |
| U201#(tt, N, X, XS) → activate#(X) | splitAt#(0, XS) → isLNat#(XS) |
| activate#(n__splitAt(X1, X2)) → splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) → U211#(isNatural(N), activate(XS)) |
| 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)) | U202#(tt, N, X, XS) → activate#(X) |
| U171#(tt, N, XS) → activate#(N) | isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) |
| activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) | U32#(tt, N) → activate#(N) |
| U101#(tt, V2) → activate#(V2) | isPLNat#(n__pair(V1, V2)) → activate#(V2) |
| U222#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) | U141#(tt, V2) → activate#(V2) |
| U202#(tt, N, X, XS) → U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) | activate#(n__head(X)) → head#(activate(X)) |
| isLNat#(n__afterNth(V1, V2)) → U41#(isNatural(activate(V1)), activate(V2)) | U151#(tt, V2) → activate#(V2) |
| U151#(tt, V2) → isLNat#(activate(V2)) | activate#(n__splitAt(X1, X2)) → activate#(X1) |
| U21#(tt, X, Y) → isLNat#(activate(Y)) | U12#(tt, N, XS) → activate#(XS) |
| U12#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | activate#(n__splitAt(X1, X2)) → activate#(X2) |
| take#(N, XS) → U221#(isNatural(N), N, XS) | isNatural#(n__head(V1)) → isLNat#(activate(V1)) |
| isLNat#(n__cons(V1, V2)) → activate#(V1) | U41#(tt, V2) → U42#(isLNat(activate(V2))) |
| U222#(tt, N, XS) → activate#(XS) | isLNat#(n__take(V1, V2)) → U101#(isNatural(activate(V1)), activate(V2)) |
| fst#(pair(X, Y)) → U21#(isLNat(X), X, Y) |
| U171#(tt, N, XS) → U172#(isLNat(activate(XS)), activate(N), activate(XS)) | sel#(N, XS) → isNatural#(N) |
| U203#(tt, N, X, XS) → U204#(splitAt(activate(N), activate(XS)), activate(X)) | isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U204#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) |
| U171#(tt, N, XS) → isLNat#(activate(XS)) | snd#(pair(X, Y)) → U181#(isLNat(X), Y) |
| U31#(tt, N, XS) → U32#(isLNat(activate(XS)), activate(N)) | U221#(tt, N, XS) → isLNat#(activate(XS)) |
| U202#(tt, N, X, XS) → isLNat#(activate(XS)) | U51#(tt, V2) → activate#(V2) |
| 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)) |
| head#(cons(N, XS)) → activate#(XS) | U201#(tt, N, X, XS) → activate#(XS) |
| snd#(pair(X, Y)) → isLNat#(X) | U31#(tt, N, XS) → isLNat#(activate(XS)) |
| U181#(tt, Y) → activate#(Y) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U172#(tt, N, XS) → activate#(N) |
| U203#(tt, N, X, XS) → activate#(N) | U202#(tt, N, X, XS) → activate#(N) |
| U101#(tt, V2) → U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) → U141#(isLNat(activate(V1)), activate(V2)) |
| U141#(tt, V2) → isLNat#(activate(V2)) | splitAt#(0, XS) → U191#(isLNat(XS), XS) |
| U211#(tt, XS) → isLNat#(activate(XS)) | activate#(n__fst(X)) → activate#(X) |
| activate#(n__sel(X1, X2)) → activate#(X2) | activate#(n__fst(X)) → fst#(activate(X)) |
| splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, activate(XS)) | activate#(n__s(X)) → activate#(X) |
| U212#(tt, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| U221#(tt, N, XS) → activate#(XS) | isNatural#(n__head(V1)) → activate#(V1) |
| natsFrom#(N) → U161#(isNatural(N), N) | natsFrom#(N) → isNatural#(N) |
| U172#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | fst#(pair(X, Y)) → isLNat#(X) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__tail(V1)) → isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) → activate#(X) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| U211#(tt, XS) → activate#(XS) | U203#(tt, N, X, XS) → activate#(X) |
| head#(cons(N, XS)) → isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) → activate#(V2) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | U181#(tt, Y) → isLNat#(activate(Y)) |
| activate#(n__take(X1, X2)) → activate#(X1) | U201#(tt, N, X, XS) → activate#(N) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| U22#(tt, X) → activate#(X) | isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| U204#(pair(YS, ZS), X) → cons#(activate(X), YS) | U181#(tt, Y) → U182#(isLNat(activate(Y)), activate(Y)) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| afterNth#(N, XS) → U11#(isNatural(N), N, XS) | U51#(tt, V2) → isLNat#(activate(V2)) |
| U211#(tt, XS) → U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U101#(tt, V2) → isLNat#(activate(V2)) | U21#(tt, X, Y) → U22#(isLNat(activate(Y)), activate(X)) |
| U131#(tt, V2) → activate#(V2) | 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) → U171#(isNatural(N), N, XS) |
| U201#(tt, N, X, XS) → U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) | U12#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) |
| U172#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) | U172#(tt, N, XS) → activate#(XS) |
| tail#(cons(N, XS)) → isNatural#(N) | isLNat#(n__take(V1, V2)) → activate#(V2) |
| U203#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | U171#(tt, N, XS) → activate#(XS) |
| U31#(tt, N, XS) → activate#(N) | U191#(tt, XS) → activate#(XS) |
| activate#(n__tail(X)) → tail#(activate(X)) | isNatural#(n__sel(V1, V2)) → activate#(V2) |
| U131#(tt, V2) → isLNat#(activate(V2)) | activate#(n__natsFrom(X)) → activate#(X) |
| isPLNat#(n__splitAt(V1, V2)) → U151#(isNatural(activate(V1)), activate(V2)) | U201#(tt, N, X, XS) → isNatural#(activate(X)) |
| U161#(tt, N) → activate#(N) | U221#(tt, N, XS) → activate#(N) |
| U21#(tt, X, Y) → activate#(Y) | U11#(tt, N, XS) → U12#(isLNat(activate(XS)), activate(N), activate(XS)) |
| U12#(tt, N, XS) → activate#(N) | U222#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| U41#(tt, V2) → isLNat#(activate(V2)) | U182#(tt, Y) → activate#(Y) |
| activate#(n__pair(X1, X2)) → activate#(X2) | U203#(tt, N, X, XS) → activate#(XS) |
| U202#(tt, N, X, XS) → activate#(XS) | U222#(tt, N, XS) → activate#(N) |
| activate#(n__pair(X1, X2)) → activate#(X1) | activate#(n__natsFrom(X)) → natsFrom#(activate(X)) |
| tail#(cons(N, XS)) → activate#(XS) | U21#(tt, X, Y) → activate#(X) |
| isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) | U221#(tt, N, XS) → U222#(isLNat(activate(XS)), activate(N), activate(XS)) |
| isNatural#(n__sel(V1, V2)) → U131#(isNatural(activate(V1)), activate(V2)) | isNatural#(n__sel(V1, V2)) → activate#(V1) |
| U31#(tt, N, XS) → activate#(XS) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| isLNat#(n__cons(V1, V2)) → U51#(isNatural(activate(V1)), activate(V2)) | isPLNat#(n__splitAt(V1, V2)) → activate#(V1) |
| U11#(tt, N, XS) → isLNat#(activate(XS)) | head#(cons(N, XS)) → U31#(isNatural(N), N, activate(XS)) |
| U41#(tt, V2) → activate#(V2) | isLNat#(n__fst(V1)) → activate#(V1) |
| U201#(tt, N, X, XS) → activate#(X) | splitAt#(0, XS) → isLNat#(XS) |
| activate#(n__splitAt(X1, X2)) → splitAt#(activate(X1), activate(X2)) | tail#(cons(N, XS)) → U211#(isNatural(N), activate(XS)) |
| U151#(tt, V2) → U152#(isLNat(activate(V2))) | 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)) |
| U202#(tt, N, X, XS) → activate#(X) | U171#(tt, N, XS) → activate#(N) |
| isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) |
| U32#(tt, N) → activate#(N) | U101#(tt, V2) → activate#(V2) |
| isPLNat#(n__pair(V1, V2)) → activate#(V2) | U222#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) |
| U141#(tt, V2) → activate#(V2) | U202#(tt, N, X, XS) → U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) |
| activate#(n__head(X)) → head#(activate(X)) | U151#(tt, V2) → isLNat#(activate(V2)) |
| U151#(tt, V2) → activate#(V2) | isLNat#(n__afterNth(V1, V2)) → U41#(isNatural(activate(V1)), activate(V2)) |
| activate#(n__splitAt(X1, X2)) → activate#(X1) | U21#(tt, X, Y) → isLNat#(activate(Y)) |
| U12#(tt, N, XS) → activate#(XS) | U12#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__splitAt(X1, X2)) → activate#(X2) | take#(N, XS) → U221#(isNatural(N), N, XS) |
| isNatural#(n__head(V1)) → isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) → activate#(V1) |
| U222#(tt, N, XS) → activate#(XS) | isLNat#(n__take(V1, V2)) → U101#(isNatural(activate(V1)), activate(V2)) |
| fst#(pair(X, Y)) → U21#(isLNat(X), X, Y) |
| U171#(tt, N, XS) → U172#(isLNat(activate(XS)), activate(N), activate(XS)) | sel#(N, XS) → isNatural#(N) |
| U203#(tt, N, X, XS) → U204#(splitAt(activate(N), activate(XS)), activate(X)) | isLNat#(n__afterNth(V1, V2)) → isNatural#(activate(V1)) |
| activate#(n__head(X)) → activate#(X) | activate#(n__tail(X)) → activate#(X) |
| afterNth#(N, XS) → isNatural#(N) | U204#(pair(YS, ZS), X) → pair#(cons(activate(X), YS), ZS) |
| U171#(tt, N, XS) → isLNat#(activate(XS)) | snd#(pair(X, Y)) → U181#(isLNat(X), Y) |
| U31#(tt, N, XS) → U32#(isLNat(activate(XS)), activate(N)) | U221#(tt, N, XS) → isLNat#(activate(XS)) |
| U202#(tt, N, X, XS) → isLNat#(activate(XS)) | U51#(tt, V2) → activate#(V2) |
| 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)) |
| head#(cons(N, XS)) → activate#(XS) | snd#(pair(X, Y)) → isLNat#(X) |
| U201#(tt, N, X, XS) → activate#(XS) | U31#(tt, N, XS) → isLNat#(activate(XS)) |
| U181#(tt, Y) → activate#(Y) | isPLNat#(n__pair(V1, V2)) → activate#(V1) |
| isLNat#(n__tail(V1)) → activate#(V1) | U172#(tt, N, XS) → activate#(N) |
| U203#(tt, N, X, XS) → activate#(N) | U202#(tt, N, X, XS) → activate#(N) |
| U101#(tt, V2) → U102#(isLNat(activate(V2))) | isPLNat#(n__pair(V1, V2)) → U141#(isLNat(activate(V1)), activate(V2)) |
| U141#(tt, V2) → isLNat#(activate(V2)) | splitAt#(0, XS) → U191#(isLNat(XS), XS) |
| U211#(tt, XS) → isLNat#(activate(XS)) | activate#(n__fst(X)) → activate#(X) |
| activate#(n__sel(X1, X2)) → activate#(X2) | activate#(n__fst(X)) → fst#(activate(X)) |
| splitAt#(s(N), cons(X, XS)) → U201#(isNatural(N), N, X, activate(XS)) | activate#(n__s(X)) → activate#(X) |
| U212#(tt, XS) → activate#(XS) | isLNat#(n__natsFrom(V1)) → activate#(V1) |
| U221#(tt, N, XS) → activate#(XS) | isNatural#(n__head(V1)) → activate#(V1) |
| natsFrom#(N) → U161#(isNatural(N), N) | natsFrom#(N) → isNatural#(N) |
| U172#(tt, N, XS) → afterNth#(activate(N), activate(XS)) | fst#(pair(X, Y)) → isLNat#(X) |
| isNatural#(n__s(V1)) → activate#(V1) | isLNat#(n__afterNth(V1, V2)) → activate#(V2) |
| isLNat#(n__tail(V1)) → isLNat#(activate(V1)) | U204#(pair(YS, ZS), X) → activate#(X) |
| isLNat#(n__cons(V1, V2)) → isNatural#(activate(V1)) | take#(N, XS) → isNatural#(N) |
| U211#(tt, XS) → activate#(XS) | U203#(tt, N, X, XS) → activate#(X) |
| head#(cons(N, XS)) → isNatural#(N) | isPLNat#(n__splitAt(V1, V2)) → activate#(V2) |
| isNatural#(n__sel(V1, V2)) → isNatural#(activate(V1)) | U181#(tt, Y) → isLNat#(activate(Y)) |
| activate#(n__take(X1, X2)) → activate#(X1) | U201#(tt, N, X, XS) → activate#(N) |
| isLNat#(n__natsFrom(V1)) → isNatural#(activate(V1)) | U11#(tt, N, XS) → activate#(XS) |
| U22#(tt, X) → activate#(X) | isPLNat#(n__splitAt(V1, V2)) → isNatural#(activate(V1)) |
| isLNat#(n__snd(V1)) → activate#(V1) | isLNat#(n__snd(V1)) → isPLNat#(activate(V1)) |
| U204#(pair(YS, ZS), X) → cons#(activate(X), YS) | U181#(tt, Y) → U182#(isLNat(activate(Y)), activate(Y)) |
| splitAt#(s(N), cons(X, XS)) → activate#(XS) | splitAt#(s(N), cons(X, XS)) → isNatural#(N) |
| afterNth#(N, XS) → U11#(isNatural(N), N, XS) | U51#(tt, V2) → isLNat#(activate(V2)) |
| U211#(tt, XS) → U212#(isLNat(activate(XS)), activate(XS)) | activate#(n__sel(X1, X2)) → activate#(X1) |
| U21#(tt, X, Y) → U22#(isLNat(activate(Y)), activate(X)) | U101#(tt, V2) → isLNat#(activate(V2)) |
| U131#(tt, V2) → activate#(V2) | activate#(n__take(X1, X2)) → take#(activate(X1), activate(X2)) |
| U51#(tt, V2) → U52#(isLNat(activate(V2))) | activate#(n__snd(X)) → snd#(activate(X)) |
| activate#(n__snd(X)) → activate#(X) | activate#(n__cons(X1, X2)) → activate#(X1) |
| sel#(N, XS) → U171#(isNatural(N), N, XS) | U201#(tt, N, X, XS) → U202#(isNatural(activate(X)), activate(N), activate(X), activate(XS)) |
| U12#(tt, N, XS) → snd#(splitAt(activate(N), activate(XS))) | U172#(tt, N, XS) → head#(afterNth(activate(N), activate(XS))) |
| U172#(tt, N, XS) → activate#(XS) | tail#(cons(N, XS)) → isNatural#(N) |
| isLNat#(n__take(V1, V2)) → activate#(V2) | U171#(tt, N, XS) → activate#(XS) |
| U203#(tt, N, X, XS) → splitAt#(activate(N), activate(XS)) | U31#(tt, N, XS) → activate#(N) |
| U191#(tt, XS) → activate#(XS) | activate#(n__tail(X)) → tail#(activate(X)) |
| isNatural#(n__sel(V1, V2)) → activate#(V2) | U131#(tt, V2) → isLNat#(activate(V2)) |
| activate#(n__natsFrom(X)) → activate#(X) | U201#(tt, N, X, XS) → isNatural#(activate(X)) |
| isPLNat#(n__splitAt(V1, V2)) → U151#(isNatural(activate(V1)), activate(V2)) | U161#(tt, N) → activate#(N) |
| U221#(tt, N, XS) → activate#(N) | U21#(tt, X, Y) → activate#(Y) |
| U11#(tt, N, XS) → U12#(isLNat(activate(XS)), activate(N), activate(XS)) | U12#(tt, N, XS) → activate#(N) |
| U222#(tt, N, XS) → splitAt#(activate(N), activate(XS)) | U41#(tt, V2) → isLNat#(activate(V2)) |
| U182#(tt, Y) → activate#(Y) | activate#(n__pair(X1, X2)) → activate#(X2) |
| U203#(tt, N, X, XS) → activate#(XS) | U202#(tt, N, X, XS) → activate#(XS) |
| U222#(tt, N, XS) → activate#(N) | activate#(n__pair(X1, X2)) → activate#(X1) |
| activate#(n__natsFrom(X)) → natsFrom#(activate(X)) | tail#(cons(N, XS)) → activate#(XS) |
| U21#(tt, X, Y) → activate#(X) | isPLNat#(n__pair(V1, V2)) → isLNat#(activate(V1)) |
| U221#(tt, N, XS) → U222#(isLNat(activate(XS)), activate(N), activate(XS)) | isNatural#(n__sel(V1, V2)) → U131#(isNatural(activate(V1)), activate(V2)) |
| isNatural#(n__sel(V1, V2)) → activate#(V1) | U31#(tt, N, XS) → activate#(XS) |
| isLNat#(n__cons(V1, V2)) → U51#(isNatural(activate(V1)), activate(V2)) | activate#(n__afterNth(X1, X2)) → activate#(X2) |
| isPLNat#(n__splitAt(V1, V2)) → activate#(V1) | U11#(tt, N, XS) → isLNat#(activate(XS)) |
| head#(cons(N, XS)) → U31#(isNatural(N), N, activate(XS)) | U41#(tt, V2) → activate#(V2) |
| isLNat#(n__fst(V1)) → activate#(V1) | U201#(tt, N, X, XS) → activate#(X) |
| splitAt#(0, XS) → isLNat#(XS) | activate#(n__splitAt(X1, X2)) → splitAt#(activate(X1), activate(X2)) |
| tail#(cons(N, XS)) → U211#(isNatural(N), activate(XS)) | 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)) |
| U202#(tt, N, X, XS) → activate#(X) | U171#(tt, N, XS) → activate#(N) |
| isLNat#(n__fst(V1)) → isPLNat#(activate(V1)) | activate#(n__sel(X1, X2)) → sel#(activate(X1), activate(X2)) |
| U32#(tt, N) → activate#(N) | U101#(tt, V2) → activate#(V2) |
| isPLNat#(n__pair(V1, V2)) → activate#(V2) | U222#(tt, N, XS) → fst#(splitAt(activate(N), activate(XS))) |
| U141#(tt, V2) → activate#(V2) | U202#(tt, N, X, XS) → U203#(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) |
| activate#(n__head(X)) → head#(activate(X)) | U151#(tt, V2) → activate#(V2) |
| U151#(tt, V2) → isLNat#(activate(V2)) | isLNat#(n__afterNth(V1, V2)) → U41#(isNatural(activate(V1)), activate(V2)) |
| activate#(n__splitAt(X1, X2)) → activate#(X1) | U21#(tt, X, Y) → isLNat#(activate(Y)) |
| U12#(tt, N, XS) → activate#(XS) | U12#(tt, N, XS) → splitAt#(activate(N), activate(XS)) |
| activate#(n__splitAt(X1, X2)) → activate#(X2) | take#(N, XS) → U221#(isNatural(N), N, XS) |
| isNatural#(n__head(V1)) → isLNat#(activate(V1)) | isLNat#(n__cons(V1, V2)) → activate#(V1) |
| U222#(tt, N, XS) → activate#(XS) | isLNat#(n__take(V1, V2)) → U101#(isNatural(activate(V1)), activate(V2)) |
| fst#(pair(X, Y)) → U21#(isLNat(X), X, Y) |