TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60016 ms.

The following DP Processors were used


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)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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




Open Dependency Pair Problem 3

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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




Open Dependency Pair Problem 4

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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




Open Dependency Pair Problem 5

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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




Open Dependency Pair Problem 6

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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




Open Dependency Pair Problem 7

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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))

Rewrite Rules

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)ttU71(tt)tt
U81(tt)ttU91(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)
niln__nilafterNth(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)0n__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)nilactivate(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

Original Signature

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

Strategy


The following SCCs where found

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)