MAYBE Time: 0.352706 TRS: { U102 tt() -> tt(), isLNat n__natsFrom V1 -> U71 isNatural activate V1, 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__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), activate X -> X, activate n__natsFrom X -> natsFrom X, activate n__nil() -> nil(), activate n__afterNth(X1, X2) -> afterNth(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__fst X -> fst X, activate n__snd X -> snd X, activate n__tail X -> tail X, activate n__take(X1, X2) -> take(X1, X2), activate n__0() -> 0(), activate n__head X -> head X, activate n__s X -> s X, activate n__sel(X1, X2) -> sel(X1, X2), activate n__pair(X1, X2) -> pair(X1, X2), activate n__splitAt(X1, X2) -> splitAt(X1, X2), U101(tt(), V2) -> U102 isLNat activate V2, U12(tt(), N, XS) -> snd splitAt(activate N, activate XS), U11(tt(), N, XS) -> U12(isLNat activate XS, activate N, activate XS), U111 tt() -> tt(), snd X -> n__snd X, snd pair(X, Y) -> U181(isLNat X, Y), splitAt(X1, X2) -> n__splitAt(X1, X2), splitAt(s N, cons(X, XS)) -> U201(isNatural N, N, X, activate XS), splitAt(0(), XS) -> U191(isLNat XS, XS), U121 tt() -> tt(), U132 tt() -> tt(), U131(tt(), V2) -> U132 isLNat activate V2, U142 tt() -> tt(), U141(tt(), V2) -> U142 isLNat activate V2, U152 tt() -> tt(), U151(tt(), V2) -> U152 isLNat activate V2, cons(X1, X2) -> n__cons(X1, X2), s X -> n__s X, U161(tt(), N) -> cons(activate N, n__natsFrom s activate N), U172(tt(), N, XS) -> head afterNth(activate N, activate XS), U171(tt(), N, XS) -> U172(isLNat activate XS, activate N, activate XS), head X -> n__head X, head cons(N, XS) -> U31(isNatural N, N, activate XS), afterNth(N, XS) -> U11(isNatural N, N, XS), afterNth(X1, X2) -> n__afterNth(X1, X2), U182(tt(), Y) -> activate Y, U181(tt(), Y) -> U182(isLNat activate Y, activate Y), pair(X1, X2) -> n__pair(X1, X2), nil() -> n__nil(), U191(tt(), XS) -> pair(nil(), activate XS), U202(tt(), N, X, XS) -> U203(isLNat activate XS, activate N, activate X, activate XS), 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), U201(tt(), N, X, XS) -> U202(isNatural activate X, 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), U22(tt(), X) -> activate X, U21(tt(), X, Y) -> U22(isLNat activate Y, activate X), U212(tt(), XS) -> activate XS, U211(tt(), XS) -> U212(isLNat activate XS, activate XS), U222(tt(), N, XS) -> fst splitAt(activate N, activate XS), U221(tt(), N, XS) -> U222(isLNat activate XS, activate N, activate XS), fst X -> n__fst X, fst pair(X, Y) -> U21(isLNat X, X, Y), U32(tt(), N) -> activate N, U31(tt(), N, XS) -> U32(isLNat activate XS, activate N), U42 tt() -> tt(), U41(tt(), V2) -> U42 isLNat activate V2, U52 tt() -> tt(), U51(tt(), V2) -> U52 isLNat activate V2, U61 tt() -> tt(), U71 tt() -> tt(), U81 tt() -> tt(), U91 tt() -> tt(), 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), natsFrom X -> n__natsFrom X, sel(N, XS) -> U171(isNatural N, N, XS), sel(X1, X2) -> n__sel(X1, X2), 0() -> n__0(), tail X -> n__tail X, tail cons(N, XS) -> U211(isNatural N, activate XS), take(N, XS) -> U221(isNatural N, N, XS), take(X1, X2) -> n__take(X1, X2)} DP: DP: { isLNat# n__natsFrom V1 -> activate# V1, isLNat# n__natsFrom V1 -> isNatural# activate V1, isLNat# n__natsFrom V1 -> U71# isNatural activate V1, isLNat# n__afterNth(V1, V2) -> activate# V2, isLNat# n__afterNth(V1, V2) -> activate# V1, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2), isLNat# n__cons(V1, V2) -> activate# V2, isLNat# n__cons(V1, V2) -> activate# V1, isLNat# n__cons(V1, V2) -> isNatural# activate V1, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2), isLNat# n__fst V1 -> activate# V1, isLNat# n__fst V1 -> U61# isPLNat activate V1, isLNat# n__fst V1 -> isPLNat# activate V1, isLNat# n__snd V1 -> activate# V1, isLNat# n__snd V1 -> U81# isPLNat activate V1, isLNat# n__snd V1 -> isPLNat# activate V1, isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__tail V1 -> activate# V1, isLNat# n__tail V1 -> U91# isLNat activate V1, isLNat# n__take(V1, V2) -> activate# V2, isLNat# n__take(V1, V2) -> activate# V1, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2), isLNat# n__take(V1, V2) -> isNatural# activate V1, activate# n__natsFrom X -> natsFrom# X, activate# n__nil() -> nil#(), activate# n__afterNth(X1, X2) -> afterNth#(X1, X2), activate# n__cons(X1, X2) -> cons#(X1, X2), activate# n__fst X -> fst# X, activate# n__snd X -> snd# X, activate# n__tail X -> tail# X, activate# n__take(X1, X2) -> take#(X1, X2), activate# n__0() -> 0#(), activate# n__head X -> head# X, activate# n__s X -> s# X, activate# n__sel(X1, X2) -> sel#(X1, X2), activate# n__pair(X1, X2) -> pair#(X1, X2), activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), U101#(tt(), V2) -> U102# isLNat activate V2, U101#(tt(), V2) -> isLNat# activate V2, U101#(tt(), V2) -> activate# V2, U12#(tt(), N, XS) -> activate# XS, U12#(tt(), N, XS) -> activate# N, U12#(tt(), N, XS) -> snd# splitAt(activate N, activate XS), U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), U11#(tt(), N, XS) -> isLNat# activate XS, U11#(tt(), N, XS) -> activate# XS, U11#(tt(), N, XS) -> activate# N, U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), snd# pair(X, Y) -> isLNat# X, snd# pair(X, Y) -> U181#(isLNat X, Y), splitAt#(s N, cons(X, XS)) -> activate# XS, splitAt#(s N, cons(X, XS)) -> isNatural# N, splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), splitAt#(0(), XS) -> isLNat# XS, splitAt#(0(), XS) -> U191#(isLNat XS, XS), U131#(tt(), V2) -> isLNat# activate V2, U131#(tt(), V2) -> activate# V2, U131#(tt(), V2) -> U132# isLNat activate V2, U141#(tt(), V2) -> isLNat# activate V2, U141#(tt(), V2) -> activate# V2, U141#(tt(), V2) -> U142# isLNat activate V2, U151#(tt(), V2) -> isLNat# activate V2, U151#(tt(), V2) -> activate# V2, U151#(tt(), V2) -> U152# isLNat activate V2, U161#(tt(), N) -> activate# N, U161#(tt(), N) -> cons#(activate N, n__natsFrom s activate N), U161#(tt(), N) -> s# activate N, U172#(tt(), N, XS) -> activate# XS, U172#(tt(), N, XS) -> activate# N, U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS), U172#(tt(), N, XS) -> afterNth#(activate N, activate XS), U171#(tt(), N, XS) -> isLNat# activate XS, U171#(tt(), N, XS) -> activate# XS, U171#(tt(), N, XS) -> activate# N, U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), head# cons(N, XS) -> activate# XS, head# cons(N, XS) -> isNatural# N, head# cons(N, XS) -> U31#(isNatural N, N, activate XS), afterNth#(N, XS) -> U11#(isNatural N, N, XS), afterNth#(N, XS) -> isNatural# N, U182#(tt(), Y) -> activate# Y, U181#(tt(), Y) -> isLNat# activate Y, U181#(tt(), Y) -> activate# Y, U181#(tt(), Y) -> U182#(isLNat activate Y, activate Y), U191#(tt(), XS) -> activate# XS, U191#(tt(), XS) -> pair#(nil(), activate XS), U191#(tt(), XS) -> nil#(), U202#(tt(), N, X, XS) -> isLNat# activate XS, U202#(tt(), N, X, XS) -> activate# XS, U202#(tt(), N, X, XS) -> activate# N, U202#(tt(), N, X, XS) -> activate# X, U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), isNatural# n__head V1 -> isLNat# activate V1, isNatural# n__head V1 -> activate# V1, isNatural# n__head V1 -> U111# isLNat activate V1, isNatural# n__s V1 -> activate# V1, isNatural# n__s V1 -> U121# isNatural activate V1, isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2, isNatural# n__sel(V1, V2) -> activate# V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2), isNatural# n__sel(V1, V2) -> isNatural# activate V1, U201#(tt(), N, X, XS) -> activate# XS, U201#(tt(), N, X, XS) -> activate# N, U201#(tt(), N, X, XS) -> activate# X, U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U201#(tt(), N, X, XS) -> isNatural# activate X, U203#(tt(), N, X, XS) -> activate# XS, U203#(tt(), N, X, XS) -> activate# N, U203#(tt(), N, X, XS) -> activate# X, U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), U203#(tt(), N, X, XS) -> U204#(splitAt(activate N, activate XS), activate X), U204#(pair(YS, ZS), X) -> activate# X, U204#(pair(YS, ZS), X) -> cons#(activate X, YS), U204#(pair(YS, ZS), X) -> pair#(cons(activate X, YS), ZS), U22#(tt(), X) -> activate# X, U21#(tt(), X, Y) -> isLNat# activate Y, U21#(tt(), X, Y) -> activate# Y, U21#(tt(), X, Y) -> activate# X, U21#(tt(), X, Y) -> U22#(isLNat activate Y, activate X), U212#(tt(), XS) -> activate# XS, U211#(tt(), XS) -> isLNat# activate XS, U211#(tt(), XS) -> activate# XS, U211#(tt(), XS) -> U212#(isLNat activate XS, activate XS), U222#(tt(), N, XS) -> activate# XS, U222#(tt(), N, XS) -> activate# N, U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), U222#(tt(), N, XS) -> fst# splitAt(activate N, activate XS), U221#(tt(), N, XS) -> isLNat# activate XS, U221#(tt(), N, XS) -> activate# XS, U221#(tt(), N, XS) -> activate# N, U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), fst# pair(X, Y) -> isLNat# X, fst# pair(X, Y) -> U21#(isLNat X, X, Y), U32#(tt(), N) -> activate# N, U31#(tt(), N, XS) -> isLNat# activate XS, U31#(tt(), N, XS) -> activate# XS, U31#(tt(), N, XS) -> activate# N, U31#(tt(), N, XS) -> U32#(isLNat activate XS, activate N), U41#(tt(), V2) -> isLNat# activate V2, U41#(tt(), V2) -> activate# V2, U41#(tt(), V2) -> U42# isLNat activate V2, U51#(tt(), V2) -> isLNat# activate V2, U51#(tt(), V2) -> activate# V2, U51#(tt(), V2) -> U52# isLNat activate V2, isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V2, isPLNat# n__pair(V1, V2) -> activate# V1, isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2), isPLNat# n__splitAt(V1, V2) -> activate# V2, isPLNat# n__splitAt(V1, V2) -> activate# V1, isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2), isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, natsFrom# N -> U161#(isNatural N, N), natsFrom# N -> isNatural# N, sel#(N, XS) -> U171#(isNatural N, N, XS), sel#(N, XS) -> isNatural# N, tail# cons(N, XS) -> activate# XS, tail# cons(N, XS) -> isNatural# N, tail# cons(N, XS) -> U211#(isNatural N, activate XS), take#(N, XS) -> isNatural# N, take#(N, XS) -> U221#(isNatural N, N, XS)} TRS: { U102 tt() -> tt(), isLNat n__natsFrom V1 -> U71 isNatural activate V1, 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__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), activate X -> X, activate n__natsFrom X -> natsFrom X, activate n__nil() -> nil(), activate n__afterNth(X1, X2) -> afterNth(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__fst X -> fst X, activate n__snd X -> snd X, activate n__tail X -> tail X, activate n__take(X1, X2) -> take(X1, X2), activate n__0() -> 0(), activate n__head X -> head X, activate n__s X -> s X, activate n__sel(X1, X2) -> sel(X1, X2), activate n__pair(X1, X2) -> pair(X1, X2), activate n__splitAt(X1, X2) -> splitAt(X1, X2), U101(tt(), V2) -> U102 isLNat activate V2, U12(tt(), N, XS) -> snd splitAt(activate N, activate XS), U11(tt(), N, XS) -> U12(isLNat activate XS, activate N, activate XS), U111 tt() -> tt(), snd X -> n__snd X, snd pair(X, Y) -> U181(isLNat X, Y), splitAt(X1, X2) -> n__splitAt(X1, X2), splitAt(s N, cons(X, XS)) -> U201(isNatural N, N, X, activate XS), splitAt(0(), XS) -> U191(isLNat XS, XS), U121 tt() -> tt(), U132 tt() -> tt(), U131(tt(), V2) -> U132 isLNat activate V2, U142 tt() -> tt(), U141(tt(), V2) -> U142 isLNat activate V2, U152 tt() -> tt(), U151(tt(), V2) -> U152 isLNat activate V2, cons(X1, X2) -> n__cons(X1, X2), s X -> n__s X, U161(tt(), N) -> cons(activate N, n__natsFrom s activate N), U172(tt(), N, XS) -> head afterNth(activate N, activate XS), U171(tt(), N, XS) -> U172(isLNat activate XS, activate N, activate XS), head X -> n__head X, head cons(N, XS) -> U31(isNatural N, N, activate XS), afterNth(N, XS) -> U11(isNatural N, N, XS), afterNth(X1, X2) -> n__afterNth(X1, X2), U182(tt(), Y) -> activate Y, U181(tt(), Y) -> U182(isLNat activate Y, activate Y), pair(X1, X2) -> n__pair(X1, X2), nil() -> n__nil(), U191(tt(), XS) -> pair(nil(), activate XS), U202(tt(), N, X, XS) -> U203(isLNat activate XS, activate N, activate X, activate XS), 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), U201(tt(), N, X, XS) -> U202(isNatural activate X, 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), U22(tt(), X) -> activate X, U21(tt(), X, Y) -> U22(isLNat activate Y, activate X), U212(tt(), XS) -> activate XS, U211(tt(), XS) -> U212(isLNat activate XS, activate XS), U222(tt(), N, XS) -> fst splitAt(activate N, activate XS), U221(tt(), N, XS) -> U222(isLNat activate XS, activate N, activate XS), fst X -> n__fst X, fst pair(X, Y) -> U21(isLNat X, X, Y), U32(tt(), N) -> activate N, U31(tt(), N, XS) -> U32(isLNat activate XS, activate N), U42 tt() -> tt(), U41(tt(), V2) -> U42 isLNat activate V2, U52 tt() -> tt(), U51(tt(), V2) -> U52 isLNat activate V2, U61 tt() -> tt(), U71 tt() -> tt(), U81 tt() -> tt(), U91 tt() -> tt(), 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), natsFrom X -> n__natsFrom X, sel(N, XS) -> U171(isNatural N, N, XS), sel(X1, X2) -> n__sel(X1, X2), 0() -> n__0(), tail X -> n__tail X, tail cons(N, XS) -> U211(isNatural N, activate XS), take(N, XS) -> U221(isNatural N, N, XS), take(X1, X2) -> n__take(X1, X2)} EDG: { (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__head X -> head# X) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__tail X -> tail# X) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__snd X -> snd# X) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__fst X -> fst# X) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isLNat# n__cons(V1, V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (U101#(tt(), V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U101#(tt(), V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U101#(tt(), V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U101#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U101#(tt(), V2) -> activate# V2, activate# n__head X -> head# X) (U101#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U101#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U101#(tt(), V2) -> activate# V2, activate# n__tail X -> tail# X) (U101#(tt(), V2) -> activate# V2, activate# n__snd X -> snd# X) (U101#(tt(), V2) -> activate# V2, activate# n__fst X -> fst# X) (U101#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U101#(tt(), V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U101#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U101#(tt(), V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (U141#(tt(), V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U141#(tt(), V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U141#(tt(), V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U141#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U141#(tt(), V2) -> activate# V2, activate# n__head X -> head# X) (U141#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U141#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U141#(tt(), V2) -> activate# V2, activate# n__tail X -> tail# X) (U141#(tt(), V2) -> activate# V2, activate# n__snd X -> snd# X) (U141#(tt(), V2) -> activate# V2, activate# n__fst X -> fst# X) (U141#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U141#(tt(), V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U141#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U141#(tt(), V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__head X -> head# X) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__tail X -> tail# X) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__snd X -> snd# X) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__fst X -> fst# X) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatural# n__sel(V1, V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (U51#(tt(), V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U51#(tt(), V2) -> activate# V2, activate# n__head X -> head# X) (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U51#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__tail X -> tail# X) (U51#(tt(), V2) -> activate# V2, activate# n__snd X -> snd# X) (U51#(tt(), V2) -> activate# V2, activate# n__fst X -> fst# X) (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U51#(tt(), V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__head X -> head# X) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__tail X -> tail# X) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__snd X -> snd# X) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__fst X -> fst# X) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isPLNat# n__splitAt(V1, V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__s X -> s# X) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__head X -> head# X) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__natsFrom V1 -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__head X -> head# X) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__cons(V1, V2) -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__snd V1 -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__snd V1 -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__snd V1 -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__snd V1 -> activate# V1, activate# n__s X -> s# X) (isLNat# n__snd V1 -> activate# V1, activate# n__head X -> head# X) (isLNat# n__snd V1 -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__snd V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__snd V1 -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__snd V1 -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__snd V1 -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__snd V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__snd V1 -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__snd V1 -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__snd V1 -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__head X -> head# X) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__take(V1, V2) -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isNatural# n__s V1 -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isNatural# n__s V1 -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isNatural# n__s V1 -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isNatural# n__s V1 -> activate# V1, activate# n__s X -> s# X) (isNatural# n__s V1 -> activate# V1, activate# n__head X -> head# X) (isNatural# n__s V1 -> activate# V1, activate# n__0() -> 0#()) (isNatural# n__s V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatural# n__s V1 -> activate# V1, activate# n__tail X -> tail# X) (isNatural# n__s V1 -> activate# V1, activate# n__snd X -> snd# X) (isNatural# n__s V1 -> activate# V1, activate# n__fst X -> fst# X) (isNatural# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatural# n__s V1 -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isNatural# n__s V1 -> activate# V1, activate# n__nil() -> nil#()) (isNatural# n__s V1 -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__head X -> head# X) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__tail X -> tail# X) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__snd X -> snd# X) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__fst X -> fst# X) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isPLNat# n__pair(V1, V2) -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (U12#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U12#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U12#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U12#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U12#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U12#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U12#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U12#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U12#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U12#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U12#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U12#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U12#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U12#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> s# X) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__head X -> head# X) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__0() -> 0#()) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__tail X -> tail# X) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__snd X -> snd# X) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__fst X -> fst# X) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__nil() -> nil#()) (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U172#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U172#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U172#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U172#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U172#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U172#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U172#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U172#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U172#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U172#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U172#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U172#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U172#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U172#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (head# cons(N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (head# cons(N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (head# cons(N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (head# cons(N, XS) -> activate# XS, activate# n__s X -> s# X) (head# cons(N, XS) -> activate# XS, activate# n__head X -> head# X) (head# cons(N, XS) -> activate# XS, activate# n__0() -> 0#()) (head# cons(N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (head# cons(N, XS) -> activate# XS, activate# n__tail X -> tail# X) (head# cons(N, XS) -> activate# XS, activate# n__snd X -> snd# X) (head# cons(N, XS) -> activate# XS, activate# n__fst X -> fst# X) (head# cons(N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (head# cons(N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (head# cons(N, XS) -> activate# XS, activate# n__nil() -> nil#()) (head# cons(N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__s X -> s# X) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__head X -> head# X) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__0() -> 0#()) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__tail X -> tail# X) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__snd X -> snd# X) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__fst X -> fst# X) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__nil() -> nil#()) (U202#(tt(), N, X, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__s X -> s# X) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__head X -> head# X) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__0() -> 0#()) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__tail X -> tail# X) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__snd X -> snd# X) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__fst X -> fst# X) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__nil() -> nil#()) (U203#(tt(), N, X, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U211#(tt(), XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U211#(tt(), XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U211#(tt(), XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U211#(tt(), XS) -> activate# XS, activate# n__s X -> s# X) (U211#(tt(), XS) -> activate# XS, activate# n__head X -> head# X) (U211#(tt(), XS) -> activate# XS, activate# n__0() -> 0#()) (U211#(tt(), XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U211#(tt(), XS) -> activate# XS, activate# n__tail X -> tail# X) (U211#(tt(), XS) -> activate# XS, activate# n__snd X -> snd# X) (U211#(tt(), XS) -> activate# XS, activate# n__fst X -> fst# X) (U211#(tt(), XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U211#(tt(), XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U211#(tt(), XS) -> activate# XS, activate# n__nil() -> nil#()) (U211#(tt(), XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U221#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U221#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U221#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U221#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U221#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U221#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U221#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U221#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U221#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U221#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U221#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U221#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U221#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U221#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (tail# cons(N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (tail# cons(N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (tail# cons(N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (tail# cons(N, XS) -> activate# XS, activate# n__s X -> s# X) (tail# cons(N, XS) -> activate# XS, activate# n__head X -> head# X) (tail# cons(N, XS) -> activate# XS, activate# n__0() -> 0#()) (tail# cons(N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (tail# cons(N, XS) -> activate# XS, activate# n__tail X -> tail# X) (tail# cons(N, XS) -> activate# XS, activate# n__snd X -> snd# X) (tail# cons(N, XS) -> activate# XS, activate# n__fst X -> fst# X) (tail# cons(N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (tail# cons(N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (tail# cons(N, XS) -> activate# XS, activate# n__nil() -> nil#()) (tail# cons(N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2), U51#(tt(), V2) -> U52# isLNat activate V2) (isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2), U51#(tt(), V2) -> activate# V2) (isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2), U51#(tt(), V2) -> isLNat# activate V2) (U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(0(), XS) -> U191#(isLNat XS, XS)) (U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(0(), XS) -> isLNat# XS) (U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS)) (U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> isNatural# N) (U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> activate# XS) (U181#(tt(), Y) -> U182#(isLNat activate Y, activate Y), U182#(tt(), Y) -> activate# Y) (isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2), U131#(tt(), V2) -> U132# isLNat activate V2) (isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2), U131#(tt(), V2) -> activate# V2) (isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2), U131#(tt(), V2) -> isLNat# activate V2) (U203#(tt(), N, X, XS) -> U204#(splitAt(activate N, activate XS), activate X), U204#(pair(YS, ZS), X) -> pair#(cons(activate X, YS), ZS)) (U203#(tt(), N, X, XS) -> U204#(splitAt(activate N, activate XS), activate X), U204#(pair(YS, ZS), X) -> cons#(activate X, YS)) (U203#(tt(), N, X, XS) -> U204#(splitAt(activate N, activate XS), activate X), U204#(pair(YS, ZS), X) -> activate# X) (U211#(tt(), XS) -> U212#(isLNat activate XS, activate XS), U212#(tt(), XS) -> activate# XS) (U31#(tt(), N, XS) -> U32#(isLNat activate XS, activate N), U32#(tt(), N) -> activate# N) (isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2), U151#(tt(), V2) -> U152# isLNat activate V2) (isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2), U151#(tt(), V2) -> activate# V2) (isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2), U151#(tt(), V2) -> isLNat# activate V2) (snd# pair(X, Y) -> U181#(isLNat X, Y), U181#(tt(), Y) -> U182#(isLNat activate Y, activate Y)) (snd# pair(X, Y) -> U181#(isLNat X, Y), U181#(tt(), Y) -> activate# Y) (snd# pair(X, Y) -> U181#(isLNat X, Y), U181#(tt(), Y) -> isLNat# activate Y) (U11#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U11#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U11#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U11#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U11#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U11#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U11#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U11#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U11#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U11#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U11#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U11#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U11#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U11#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U161#(tt(), N) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U161#(tt(), N) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U161#(tt(), N) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U161#(tt(), N) -> activate# N, activate# n__s X -> s# X) (U161#(tt(), N) -> activate# N, activate# n__head X -> head# X) (U161#(tt(), N) -> activate# N, activate# n__0() -> 0#()) (U161#(tt(), N) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U161#(tt(), N) -> activate# N, activate# n__tail X -> tail# X) (U161#(tt(), N) -> activate# N, activate# n__snd X -> snd# X) (U161#(tt(), N) -> activate# N, activate# n__fst X -> fst# X) (U161#(tt(), N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U161#(tt(), N) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U161#(tt(), N) -> activate# N, activate# n__nil() -> nil#()) (U161#(tt(), N) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U171#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U171#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U171#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U171#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U171#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U171#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U171#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U171#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U171#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U171#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U171#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U171#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U171#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U171#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (afterNth#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (afterNth#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (afterNth#(N, XS) -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__s V1 -> activate# V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__head V1 -> activate# V1) (afterNth#(N, XS) -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (U201#(tt(), N, X, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# N, activate# n__s X -> s# X) (U201#(tt(), N, X, XS) -> activate# N, activate# n__head X -> head# X) (U201#(tt(), N, X, XS) -> activate# N, activate# n__0() -> 0#()) (U201#(tt(), N, X, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# N, activate# n__tail X -> tail# X) (U201#(tt(), N, X, XS) -> activate# N, activate# n__snd X -> snd# X) (U201#(tt(), N, X, XS) -> activate# N, activate# n__fst X -> fst# X) (U201#(tt(), N, X, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# N, activate# n__nil() -> nil#()) (U201#(tt(), N, X, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U222#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U222#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U222#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U222#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U222#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U222#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U222#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U222#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U222#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U222#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U222#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U222#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U222#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U222#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U32#(tt(), N) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U32#(tt(), N) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U32#(tt(), N) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U32#(tt(), N) -> activate# N, activate# n__s X -> s# X) (U32#(tt(), N) -> activate# N, activate# n__head X -> head# X) (U32#(tt(), N) -> activate# N, activate# n__0() -> 0#()) (U32#(tt(), N) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U32#(tt(), N) -> activate# N, activate# n__tail X -> tail# X) (U32#(tt(), N) -> activate# N, activate# n__snd X -> snd# X) (U32#(tt(), N) -> activate# N, activate# n__fst X -> fst# X) (U32#(tt(), N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U32#(tt(), N) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U32#(tt(), N) -> activate# N, activate# n__nil() -> nil#()) (U32#(tt(), N) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (natsFrom# N -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (natsFrom# N -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (natsFrom# N -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (natsFrom# N -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (natsFrom# N -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (natsFrom# N -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (natsFrom# N -> isNatural# N, isNatural# n__s V1 -> activate# V1) (natsFrom# N -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (natsFrom# N -> isNatural# N, isNatural# n__head V1 -> activate# V1) (natsFrom# N -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (tail# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (tail# cons(N, XS) -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__s V1 -> activate# V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__head V1 -> activate# V1) (tail# cons(N, XS) -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (natsFrom# N -> U161#(isNatural N, N), U161#(tt(), N) -> s# activate N) (natsFrom# N -> U161#(isNatural N, N), U161#(tt(), N) -> cons#(activate N, n__natsFrom s activate N)) (natsFrom# N -> U161#(isNatural N, N), U161#(tt(), N) -> activate# N) (U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), U172#(tt(), N, XS) -> afterNth#(activate N, activate XS)) (U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS)) (U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), U172#(tt(), N, XS) -> activate# N) (U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), U172#(tt(), N, XS) -> activate# XS) (U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), U222#(tt(), N, XS) -> fst# splitAt(activate N, activate XS)) (U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), U222#(tt(), N, XS) -> splitAt#(activate N, activate XS)) (U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), U222#(tt(), N, XS) -> activate# N) (U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), U222#(tt(), N, XS) -> activate# XS) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2)) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> activate# V1) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> activate# V2) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2)) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V1) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V2) (isLNat# n__fst V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> isLNat# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> isNatural# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> activate# V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> activate# V2) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__tail V1 -> U91# isLNat activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__tail V1 -> activate# V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__tail V1 -> isLNat# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__snd V1 -> isPLNat# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__snd V1 -> U81# isPLNat activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__snd V1 -> activate# V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__fst V1 -> isPLNat# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__fst V1 -> U61# isPLNat activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__fst V1 -> activate# V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> activate# V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> activate# V2) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V2) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__natsFrom V1 -> isNatural# activate V1) (isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__natsFrom V1 -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> isNatural# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__take(V1, V2) -> activate# V2) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__tail V1 -> U91# isLNat activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__tail V1 -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__tail V1 -> isLNat# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__snd V1 -> isPLNat# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__snd V1 -> U81# isPLNat activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__snd V1 -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__fst V1 -> isPLNat# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__fst V1 -> U61# isPLNat activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__fst V1 -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> activate# V2) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V2) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__natsFrom V1 -> isNatural# activate V1) (isNatural# n__head V1 -> isLNat# activate V1, isLNat# n__natsFrom V1 -> activate# V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isNatural# n__sel(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> activate# V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> activate# V2) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__tail V1 -> U91# isLNat activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__tail V1 -> activate# V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__tail V1 -> isLNat# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__snd V1 -> isPLNat# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__snd V1 -> activate# V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__fst V1 -> isPLNat# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__fst V1 -> activate# V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> activate# V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> activate# V2) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> activate# V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> activate# V2) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U181#(tt(), Y) -> isLNat# activate Y, isLNat# n__natsFrom V1 -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V2) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> isLNat# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> isPLNat# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> isPLNat# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V2) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U171#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V2) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__tail V1 -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__tail V1 -> isLNat# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__snd V1 -> isPLNat# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__snd V1 -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__fst V1 -> isPLNat# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__fst V1 -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V2) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U211#(tt(), XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V2) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> isLNat# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> isPLNat# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> isPLNat# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V2) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U31#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V2) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> U91# isLNat activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> isLNat# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> isPLNat# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> isPLNat# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V2) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V2) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U131#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V2) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> U91# isLNat activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> isLNat# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> isPLNat# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> isPLNat# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V2) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V2) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U151#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V2) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> U91# isLNat activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> isLNat# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> isPLNat# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> isPLNat# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V2) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V2) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U51#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> activate# V1) (U12#(tt(), N, XS) -> snd# splitAt(activate N, activate XS), snd# pair(X, Y) -> U181#(isLNat X, Y)) (U12#(tt(), N, XS) -> snd# splitAt(activate N, activate XS), snd# pair(X, Y) -> isLNat# X) (U222#(tt(), N, XS) -> fst# splitAt(activate N, activate XS), fst# pair(X, Y) -> U21#(isLNat X, X, Y)) (U222#(tt(), N, XS) -> fst# splitAt(activate N, activate XS), fst# pair(X, Y) -> isLNat# X) (U181#(tt(), Y) -> activate# Y, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U181#(tt(), Y) -> activate# Y, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U181#(tt(), Y) -> activate# Y, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U181#(tt(), Y) -> activate# Y, activate# n__s X -> s# X) (U181#(tt(), Y) -> activate# Y, activate# n__head X -> head# X) (U181#(tt(), Y) -> activate# Y, activate# n__0() -> 0#()) (U181#(tt(), Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2)) (U181#(tt(), Y) -> activate# Y, activate# n__tail X -> tail# X) (U181#(tt(), Y) -> activate# Y, activate# n__snd X -> snd# X) (U181#(tt(), Y) -> activate# Y, activate# n__fst X -> fst# X) (U181#(tt(), Y) -> activate# Y, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U181#(tt(), Y) -> activate# Y, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U181#(tt(), Y) -> activate# Y, activate# n__nil() -> nil#()) (U181#(tt(), Y) -> activate# Y, activate# n__natsFrom X -> natsFrom# X) (fst# pair(X, Y) -> U21#(isLNat X, X, Y), U21#(tt(), X, Y) -> U22#(isLNat activate Y, activate X)) (fst# pair(X, Y) -> U21#(isLNat X, X, Y), U21#(tt(), X, Y) -> activate# X) (fst# pair(X, Y) -> U21#(isLNat X, X, Y), U21#(tt(), X, Y) -> activate# Y) (fst# pair(X, Y) -> U21#(isLNat X, X, Y), U21#(tt(), X, Y) -> isLNat# activate Y) (sel#(N, XS) -> U171#(isNatural N, N, XS), U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS)) (sel#(N, XS) -> U171#(isNatural N, N, XS), U171#(tt(), N, XS) -> activate# N) (sel#(N, XS) -> U171#(isNatural N, N, XS), U171#(tt(), N, XS) -> activate# XS) (sel#(N, XS) -> U171#(isNatural N, N, XS), U171#(tt(), N, XS) -> isLNat# activate XS) (activate# n__natsFrom X -> natsFrom# X, natsFrom# N -> isNatural# N) (activate# n__natsFrom X -> natsFrom# X, natsFrom# N -> U161#(isNatural N, N)) (activate# n__snd X -> snd# X, snd# pair(X, Y) -> U181#(isLNat X, Y)) (activate# n__snd X -> snd# X, snd# pair(X, Y) -> isLNat# X) (activate# n__head X -> head# X, head# cons(N, XS) -> U31#(isNatural N, N, activate XS)) (activate# n__head X -> head# X, head# cons(N, XS) -> isNatural# N) (activate# n__head X -> head# X, head# cons(N, XS) -> activate# XS) (snd# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> isNatural# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (snd# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> activate# V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> activate# V2) (snd# pair(X, Y) -> isLNat# X, isLNat# n__tail V1 -> U91# isLNat activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__tail V1 -> activate# V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__tail V1 -> isLNat# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__snd V1 -> isPLNat# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__snd V1 -> U81# isPLNat activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__snd V1 -> activate# V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__fst V1 -> isPLNat# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__fst V1 -> U61# isPLNat activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__fst V1 -> activate# V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (snd# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> activate# V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> activate# V2) (snd# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (snd# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> activate# V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> activate# V2) (snd# pair(X, Y) -> isLNat# X, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__natsFrom V1 -> isNatural# activate V1) (snd# pair(X, Y) -> isLNat# X, isLNat# n__natsFrom V1 -> activate# V1) (U201#(tt(), N, X, XS) -> activate# X, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# X, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# X, activate# n__s X -> s# X) (U201#(tt(), N, X, XS) -> activate# X, activate# n__head X -> head# X) (U201#(tt(), N, X, XS) -> activate# X, activate# n__0() -> 0#()) (U201#(tt(), N, X, XS) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# X, activate# n__tail X -> tail# X) (U201#(tt(), N, X, XS) -> activate# X, activate# n__snd X -> snd# X) (U201#(tt(), N, X, XS) -> activate# X, activate# n__fst X -> fst# X) (U201#(tt(), N, X, XS) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# X, activate# n__nil() -> nil#()) (U201#(tt(), N, X, XS) -> activate# X, activate# n__natsFrom X -> natsFrom# X) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__s X -> s# X) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__head X -> head# X) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__0() -> 0#()) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2)) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__tail X -> tail# X) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__snd X -> snd# X) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__fst X -> fst# X) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__nil() -> nil#()) (U204#(pair(YS, ZS), X) -> activate# X, activate# n__natsFrom X -> natsFrom# X) (U21#(tt(), X, Y) -> activate# X, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U21#(tt(), X, Y) -> activate# X, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U21#(tt(), X, Y) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U21#(tt(), X, Y) -> activate# X, activate# n__s X -> s# X) (U21#(tt(), X, Y) -> activate# X, activate# n__head X -> head# X) (U21#(tt(), X, Y) -> activate# X, activate# n__0() -> 0#()) (U21#(tt(), X, Y) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2)) (U21#(tt(), X, Y) -> activate# X, activate# n__tail X -> tail# X) (U21#(tt(), X, Y) -> activate# X, activate# n__snd X -> snd# X) (U21#(tt(), X, Y) -> activate# X, activate# n__fst X -> fst# X) (U21#(tt(), X, Y) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U21#(tt(), X, Y) -> activate# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U21#(tt(), X, Y) -> activate# X, activate# n__nil() -> nil#()) (U21#(tt(), X, Y) -> activate# X, activate# n__natsFrom X -> natsFrom# X) (activate# n__afterNth(X1, X2) -> afterNth#(X1, X2), afterNth#(N, XS) -> isNatural# N) (activate# n__afterNth(X1, X2) -> afterNth#(X1, X2), afterNth#(N, XS) -> U11#(isNatural N, N, XS)) (activate# n__take(X1, X2) -> take#(X1, X2), take#(N, XS) -> U221#(isNatural N, N, XS)) (activate# n__take(X1, X2) -> take#(X1, X2), take#(N, XS) -> isNatural# N) (splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), U201#(tt(), N, X, XS) -> isNatural# activate X) (splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS)) (splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), U201#(tt(), N, X, XS) -> activate# X) (splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), U201#(tt(), N, X, XS) -> activate# N) (splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), U201#(tt(), N, X, XS) -> 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)) (U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U202#(tt(), N, X, XS) -> activate# X) (U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U202#(tt(), N, X, XS) -> activate# N) (U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U202#(tt(), N, X, XS) -> activate# XS) (U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U202#(tt(), N, X, XS) -> isLNat# activate XS) (U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), U203#(tt(), N, X, XS) -> activate# XS) (U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), U203#(tt(), N, X, XS) -> activate# N) (U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), U203#(tt(), N, X, XS) -> activate# X) (U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), U203#(tt(), N, X, XS) -> splitAt#(activate N, 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)) (activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), splitAt#(s N, cons(X, XS)) -> activate# XS) (activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), splitAt#(s N, cons(X, XS)) -> isNatural# N) (activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS)) (activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), splitAt#(0(), XS) -> isLNat# XS) (activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), splitAt#(0(), XS) -> U191#(isLNat XS, XS)) (activate# n__sel(X1, X2) -> sel#(X1, X2), sel#(N, XS) -> U171#(isNatural N, N, XS)) (activate# n__sel(X1, X2) -> sel#(X1, X2), sel#(N, XS) -> isNatural# N) (fst# pair(X, Y) -> isLNat# X, isLNat# n__natsFrom V1 -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__natsFrom V1 -> isNatural# activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> activate# V2) (fst# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (fst# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> activate# V2) (fst# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (fst# pair(X, Y) -> isLNat# X, isLNat# n__fst V1 -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__fst V1 -> U61# isPLNat activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__fst V1 -> isPLNat# activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__snd V1 -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__snd V1 -> U81# isPLNat activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__snd V1 -> isPLNat# activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__tail V1 -> isLNat# activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__tail V1 -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__tail V1 -> U91# isLNat activate V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> activate# V2) (fst# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> activate# V1) (fst# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (fst# pair(X, Y) -> isLNat# X, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U22#(tt(), X) -> activate# X, activate# n__natsFrom X -> natsFrom# X) (U22#(tt(), X) -> activate# X, activate# n__nil() -> nil#()) (U22#(tt(), X) -> activate# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U22#(tt(), X) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U22#(tt(), X) -> activate# X, activate# n__fst X -> fst# X) (U22#(tt(), X) -> activate# X, activate# n__snd X -> snd# X) (U22#(tt(), X) -> activate# X, activate# n__tail X -> tail# X) (U22#(tt(), X) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2)) (U22#(tt(), X) -> activate# X, activate# n__0() -> 0#()) (U22#(tt(), X) -> activate# X, activate# n__head X -> head# X) (U22#(tt(), X) -> activate# X, activate# n__s X -> s# X) (U22#(tt(), X) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U22#(tt(), X) -> activate# X, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U22#(tt(), X) -> activate# X, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# X, activate# n__natsFrom X -> natsFrom# X) (U203#(tt(), N, X, XS) -> activate# X, activate# n__nil() -> nil#()) (U203#(tt(), N, X, XS) -> activate# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# X, activate# n__fst X -> fst# X) (U203#(tt(), N, X, XS) -> activate# X, activate# n__snd X -> snd# X) (U203#(tt(), N, X, XS) -> activate# X, activate# n__tail X -> tail# X) (U203#(tt(), N, X, XS) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# X, activate# n__0() -> 0#()) (U203#(tt(), N, X, XS) -> activate# X, activate# n__head X -> head# X) (U203#(tt(), N, X, XS) -> activate# X, activate# n__s X -> s# X) (U203#(tt(), N, X, XS) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# X, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# X, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# X, activate# n__natsFrom X -> natsFrom# X) (U202#(tt(), N, X, XS) -> activate# X, activate# n__nil() -> nil#()) (U202#(tt(), N, X, XS) -> activate# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# X, activate# n__fst X -> fst# X) (U202#(tt(), N, X, XS) -> activate# X, activate# n__snd X -> snd# X) (U202#(tt(), N, X, XS) -> activate# X, activate# n__tail X -> tail# X) (U202#(tt(), N, X, XS) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# X, activate# n__0() -> 0#()) (U202#(tt(), N, X, XS) -> activate# X, activate# n__head X -> head# X) (U202#(tt(), N, X, XS) -> activate# X, activate# n__s X -> s# X) (U202#(tt(), N, X, XS) -> activate# X, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# X, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# X, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (activate# n__tail X -> tail# X, tail# cons(N, XS) -> activate# XS) (activate# n__tail X -> tail# X, tail# cons(N, XS) -> isNatural# N) (activate# n__tail X -> tail# X, tail# cons(N, XS) -> U211#(isNatural N, activate XS)) (activate# n__fst X -> fst# X, fst# pair(X, Y) -> isLNat# X) (activate# n__fst X -> fst# X, fst# pair(X, Y) -> U21#(isLNat X, X, Y)) (take#(N, XS) -> U221#(isNatural N, N, XS), U221#(tt(), N, XS) -> isLNat# activate XS) (take#(N, XS) -> U221#(isNatural N, N, XS), U221#(tt(), N, XS) -> activate# XS) (take#(N, XS) -> U221#(isNatural N, N, XS), U221#(tt(), N, XS) -> activate# N) (take#(N, XS) -> U221#(isNatural N, N, XS), U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS)) (afterNth#(N, XS) -> U11#(isNatural N, N, XS), U11#(tt(), N, XS) -> isLNat# activate XS) (afterNth#(N, XS) -> U11#(isNatural N, N, XS), U11#(tt(), N, XS) -> activate# XS) (afterNth#(N, XS) -> U11#(isNatural N, N, XS), U11#(tt(), N, XS) -> activate# N) (afterNth#(N, XS) -> U11#(isNatural N, N, XS), U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS)) (U21#(tt(), X, Y) -> activate# Y, activate# n__natsFrom X -> natsFrom# X) (U21#(tt(), X, Y) -> activate# Y, activate# n__nil() -> nil#()) (U21#(tt(), X, Y) -> activate# Y, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U21#(tt(), X, Y) -> activate# Y, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U21#(tt(), X, Y) -> activate# Y, activate# n__fst X -> fst# X) (U21#(tt(), X, Y) -> activate# Y, activate# n__snd X -> snd# X) (U21#(tt(), X, Y) -> activate# Y, activate# n__tail X -> tail# X) (U21#(tt(), X, Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2)) (U21#(tt(), X, Y) -> activate# Y, activate# n__0() -> 0#()) (U21#(tt(), X, Y) -> activate# Y, activate# n__head X -> head# X) (U21#(tt(), X, Y) -> activate# Y, activate# n__s X -> s# X) (U21#(tt(), X, Y) -> activate# Y, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U21#(tt(), X, Y) -> activate# Y, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U21#(tt(), X, Y) -> activate# Y, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U182#(tt(), Y) -> activate# Y, activate# n__natsFrom X -> natsFrom# X) (U182#(tt(), Y) -> activate# Y, activate# n__nil() -> nil#()) (U182#(tt(), Y) -> activate# Y, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U182#(tt(), Y) -> activate# Y, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U182#(tt(), Y) -> activate# Y, activate# n__fst X -> fst# X) (U182#(tt(), Y) -> activate# Y, activate# n__snd X -> snd# X) (U182#(tt(), Y) -> activate# Y, activate# n__tail X -> tail# X) (U182#(tt(), Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2)) (U182#(tt(), Y) -> activate# Y, activate# n__0() -> 0#()) (U182#(tt(), Y) -> activate# Y, activate# n__head X -> head# X) (U182#(tt(), Y) -> activate# Y, activate# n__s X -> s# X) (U182#(tt(), Y) -> activate# Y, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U182#(tt(), Y) -> activate# Y, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U182#(tt(), Y) -> activate# Y, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS), head# cons(N, XS) -> activate# XS) (U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS), head# cons(N, XS) -> isNatural# N) (U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS), head# cons(N, XS) -> U31#(isNatural N, N, activate XS)) (splitAt#(0(), XS) -> U191#(isLNat XS, XS), U191#(tt(), XS) -> activate# XS) (splitAt#(0(), XS) -> U191#(isLNat XS, XS), U191#(tt(), XS) -> pair#(nil(), activate XS)) (splitAt#(0(), XS) -> U191#(isLNat XS, XS), U191#(tt(), XS) -> nil#()) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V2) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V2) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> isPLNat# activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> isPLNat# activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> isLNat# activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> U91# isLNat activate V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V2) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V1) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U41#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V2) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V2) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> isPLNat# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> isPLNat# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> isLNat# activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> U91# isLNat activate V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V2) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V1) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U141#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V2) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V2) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__fst V1 -> isPLNat# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__snd V1 -> isPLNat# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> isLNat# activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__tail V1 -> U91# isLNat activate V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V2) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> activate# V1) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U101#(tt(), V2) -> isLNat# activate V2, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V2) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> isPLNat# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> isPLNat# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> isLNat# activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V2) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V1) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U221#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V2) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> isPLNat# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> isPLNat# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> isLNat# activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V2) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V1) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U202#(tt(), N, X, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V2) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__fst V1 -> isPLNat# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__snd V1 -> isPLNat# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> isLNat# activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V2) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> activate# V1) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U11#(tt(), N, XS) -> isLNat# activate XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__natsFrom V1 -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__natsFrom V1 -> isNatural# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> activate# V2) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> activate# V2) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__fst V1 -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__fst V1 -> U61# isPLNat activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__fst V1 -> isPLNat# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__snd V1 -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__snd V1 -> U81# isPLNat activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__snd V1 -> isPLNat# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__tail V1 -> isLNat# activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__tail V1 -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__tail V1 -> U91# isLNat activate V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> activate# V2) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> activate# V1) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (U21#(tt(), X, Y) -> isLNat# activate Y, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__head V1 -> isLNat# activate V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__head V1 -> activate# V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__head V1 -> U111# isLNat activate V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__s V1 -> activate# V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__s V1 -> U121# isNatural activate V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__s V1 -> isNatural# activate V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__sel(V1, V2) -> activate# V2) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__sel(V1, V2) -> activate# V1) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (U201#(tt(), N, X, XS) -> isNatural# activate X, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__natsFrom V1 -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__natsFrom V1 -> isNatural# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V2) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> activate# V2) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__fst V1 -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__fst V1 -> U61# isPLNat activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__fst V1 -> isPLNat# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__snd V1 -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__snd V1 -> U81# isPLNat activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__snd V1 -> isPLNat# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__tail V1 -> isLNat# activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__tail V1 -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__tail V1 -> U91# isLNat activate V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__take(V1, V2) -> activate# V2) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__take(V1, V2) -> activate# V1) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isLNat# n__take(V1, V2) -> isNatural# activate V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isLNat# n__take(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> isLNat# activate V1) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V2) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V1) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2)) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> activate# V2) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> activate# V1) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2)) (isLNat# n__snd V1 -> isPLNat# activate V1, isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isLNat# n__cons(V1, V2) -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__head V1 -> isLNat# activate V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__head V1 -> activate# V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__head V1 -> U111# isLNat activate V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__s V1 -> activate# V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__s V1 -> U121# isNatural activate V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__s V1 -> isNatural# activate V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V1) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (isLNat# n__natsFrom V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (head# cons(N, XS) -> U31#(isNatural N, N, activate XS), U31#(tt(), N, XS) -> isLNat# activate XS) (head# cons(N, XS) -> U31#(isNatural N, N, activate XS), U31#(tt(), N, XS) -> activate# XS) (head# cons(N, XS) -> U31#(isNatural N, N, activate XS), U31#(tt(), N, XS) -> activate# N) (head# cons(N, XS) -> U31#(isNatural N, N, activate XS), U31#(tt(), N, XS) -> U32#(isLNat activate XS, activate N)) (U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), U12#(tt(), N, XS) -> activate# XS) (U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), U12#(tt(), N, XS) -> activate# N) (U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), U12#(tt(), N, XS) -> snd# splitAt(activate N, activate XS)) (U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), U12#(tt(), N, XS) -> splitAt#(activate N, activate XS)) (take#(N, XS) -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (take#(N, XS) -> isNatural# N, isNatural# n__head V1 -> activate# V1) (take#(N, XS) -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (take#(N, XS) -> isNatural# N, isNatural# n__s V1 -> activate# V1) (take#(N, XS) -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (take#(N, XS) -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (take#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (take#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (take#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (take#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (sel#(N, XS) -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (sel#(N, XS) -> isNatural# N, isNatural# n__head V1 -> activate# V1) (sel#(N, XS) -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (sel#(N, XS) -> isNatural# N, isNatural# n__s V1 -> activate# V1) (sel#(N, XS) -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (sel#(N, XS) -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (sel#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (sel#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (sel#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (sel#(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (U31#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U31#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U31#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U31#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U31#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U31#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U31#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U31#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U31#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U31#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U31#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U31#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U31#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U31#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U221#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U221#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U221#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U221#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U221#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U221#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U221#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U221#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U221#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U221#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U221#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U221#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U221#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U221#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U203#(tt(), N, X, XS) -> activate# N, activate# n__nil() -> nil#()) (U203#(tt(), N, X, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# N, activate# n__fst X -> fst# X) (U203#(tt(), N, X, XS) -> activate# N, activate# n__snd X -> snd# X) (U203#(tt(), N, X, XS) -> activate# N, activate# n__tail X -> tail# X) (U203#(tt(), N, X, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# N, activate# n__0() -> 0#()) (U203#(tt(), N, X, XS) -> activate# N, activate# n__head X -> head# X) (U203#(tt(), N, X, XS) -> activate# N, activate# n__s X -> s# X) (U203#(tt(), N, X, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U203#(tt(), N, X, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U202#(tt(), N, X, XS) -> activate# N, activate# n__nil() -> nil#()) (U202#(tt(), N, X, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# N, activate# n__fst X -> fst# X) (U202#(tt(), N, X, XS) -> activate# N, activate# n__snd X -> snd# X) (U202#(tt(), N, X, XS) -> activate# N, activate# n__tail X -> tail# X) (U202#(tt(), N, X, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# N, activate# n__0() -> 0#()) (U202#(tt(), N, X, XS) -> activate# N, activate# n__head X -> head# X) (U202#(tt(), N, X, XS) -> activate# N, activate# n__s X -> s# X) (U202#(tt(), N, X, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U202#(tt(), N, X, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (head# cons(N, XS) -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__head V1 -> activate# V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__s V1 -> activate# V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (head# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (head# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (head# cons(N, XS) -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (U172#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U172#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U172#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U172#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U172#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U172#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U172#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U172#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U172#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U172#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U172#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U172#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U172#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U172#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__head V1 -> isLNat# activate V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__head V1 -> activate# V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__head V1 -> U111# isLNat activate V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__s V1 -> activate# V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__s V1 -> U121# isNatural activate V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__s V1 -> isNatural# activate V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V2) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__sel(V1, V2) -> activate# V1) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2)) (splitAt#(s N, cons(X, XS)) -> isNatural# N, isNatural# n__sel(V1, V2) -> isNatural# activate V1) (U12#(tt(), N, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X) (U12#(tt(), N, XS) -> activate# N, activate# n__nil() -> nil#()) (U12#(tt(), N, XS) -> activate# N, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U12#(tt(), N, XS) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U12#(tt(), N, XS) -> activate# N, activate# n__fst X -> fst# X) (U12#(tt(), N, XS) -> activate# N, activate# n__snd X -> snd# X) (U12#(tt(), N, XS) -> activate# N, activate# n__tail X -> tail# X) (U12#(tt(), N, XS) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2)) (U12#(tt(), N, XS) -> activate# N, activate# n__0() -> 0#()) (U12#(tt(), N, XS) -> activate# N, activate# n__head X -> head# X) (U12#(tt(), N, XS) -> activate# N, activate# n__s X -> s# X) (U12#(tt(), N, XS) -> activate# N, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U12#(tt(), N, XS) -> activate# N, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U12#(tt(), N, XS) -> activate# N, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (tail# cons(N, XS) -> U211#(isNatural N, activate XS), U211#(tt(), XS) -> isLNat# activate XS) (tail# cons(N, XS) -> U211#(isNatural N, activate XS), U211#(tt(), XS) -> activate# XS) (tail# cons(N, XS) -> U211#(isNatural N, activate XS), U211#(tt(), XS) -> U212#(isLNat activate XS, activate XS)) (isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2), U141#(tt(), V2) -> isLNat# activate V2) (isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2), U141#(tt(), V2) -> activate# V2) (isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2), U141#(tt(), V2) -> U142# isLNat activate V2) (U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> activate# XS) (U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> isNatural# N) (U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS)) (U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(0(), XS) -> isLNat# XS) (U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), splitAt#(0(), XS) -> U191#(isLNat XS, XS)) (U21#(tt(), X, Y) -> U22#(isLNat activate Y, activate X), U22#(tt(), X) -> activate# X) (U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> activate# XS) (U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> isNatural# N) (U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS)) (U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(0(), XS) -> isLNat# XS) (U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(0(), XS) -> U191#(isLNat XS, XS)) (U172#(tt(), N, XS) -> afterNth#(activate N, activate XS), afterNth#(N, XS) -> U11#(isNatural N, N, XS)) (U172#(tt(), N, XS) -> afterNth#(activate N, activate XS), afterNth#(N, XS) -> isNatural# N) (isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2), U101#(tt(), V2) -> U102# isLNat activate V2) (isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2), U101#(tt(), V2) -> isLNat# activate V2) (isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2), U101#(tt(), V2) -> activate# V2) (isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2), U41#(tt(), V2) -> isLNat# activate V2) (isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2), U41#(tt(), V2) -> activate# V2) (isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2), U41#(tt(), V2) -> U42# isLNat activate V2) (U31#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U31#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U31#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U31#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U31#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U31#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U31#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U31#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U31#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U31#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U31#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U31#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U31#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U31#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U222#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U222#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U222#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U222#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U222#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U222#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U222#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U222#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U222#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U222#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U222#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U222#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U222#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U222#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U212#(tt(), XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U212#(tt(), XS) -> activate# XS, activate# n__nil() -> nil#()) (U212#(tt(), XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U212#(tt(), XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U212#(tt(), XS) -> activate# XS, activate# n__fst X -> fst# X) (U212#(tt(), XS) -> activate# XS, activate# n__snd X -> snd# X) (U212#(tt(), XS) -> activate# XS, activate# n__tail X -> tail# X) (U212#(tt(), XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U212#(tt(), XS) -> activate# XS, activate# n__0() -> 0#()) (U212#(tt(), XS) -> activate# XS, activate# n__head X -> head# X) (U212#(tt(), XS) -> activate# XS, activate# n__s X -> s# X) (U212#(tt(), XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U212#(tt(), XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U212#(tt(), XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__nil() -> nil#()) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__fst X -> fst# X) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__snd X -> snd# X) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__tail X -> tail# X) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__0() -> 0#()) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__head X -> head# X) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__s X -> s# X) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U201#(tt(), N, X, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U191#(tt(), XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U191#(tt(), XS) -> activate# XS, activate# n__nil() -> nil#()) (U191#(tt(), XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U191#(tt(), XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U191#(tt(), XS) -> activate# XS, activate# n__fst X -> fst# X) (U191#(tt(), XS) -> activate# XS, activate# n__snd X -> snd# X) (U191#(tt(), XS) -> activate# XS, activate# n__tail X -> tail# X) (U191#(tt(), XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U191#(tt(), XS) -> activate# XS, activate# n__0() -> 0#()) (U191#(tt(), XS) -> activate# XS, activate# n__head X -> head# X) (U191#(tt(), XS) -> activate# XS, activate# n__s X -> s# X) (U191#(tt(), XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U191#(tt(), XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U191#(tt(), XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U171#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U171#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U171#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U171#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U171#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U171#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U171#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U171#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U171#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U171#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U171#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U171#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U171#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U171#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__natsFrom V1 -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__natsFrom V1 -> isNatural# activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__natsFrom V1 -> U71# isNatural activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__afterNth(V1, V2) -> activate# V2) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__afterNth(V1, V2) -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2)) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__cons(V1, V2) -> activate# V2) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__cons(V1, V2) -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__cons(V1, V2) -> isNatural# activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2)) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__fst V1 -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__fst V1 -> U61# isPLNat activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__fst V1 -> isPLNat# activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__snd V1 -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__snd V1 -> U81# isPLNat activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__snd V1 -> isPLNat# activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__tail V1 -> isLNat# activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__tail V1 -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__tail V1 -> U91# isLNat activate V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__take(V1, V2) -> activate# V2) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__take(V1, V2) -> activate# V1) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2)) (splitAt#(0(), XS) -> isLNat# XS, isLNat# n__take(V1, V2) -> isNatural# activate V1) (U11#(tt(), N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X) (U11#(tt(), N, XS) -> activate# XS, activate# n__nil() -> nil#()) (U11#(tt(), N, XS) -> activate# XS, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U11#(tt(), N, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U11#(tt(), N, XS) -> activate# XS, activate# n__fst X -> fst# X) (U11#(tt(), N, XS) -> activate# XS, activate# n__snd X -> snd# X) (U11#(tt(), N, XS) -> activate# XS, activate# n__tail X -> tail# X) (U11#(tt(), N, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (U11#(tt(), N, XS) -> activate# XS, activate# n__0() -> 0#()) (U11#(tt(), N, XS) -> activate# XS, activate# n__head X -> head# X) (U11#(tt(), N, XS) -> activate# XS, activate# n__s X -> s# X) (U11#(tt(), N, XS) -> activate# XS, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U11#(tt(), N, XS) -> activate# XS, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U11#(tt(), N, XS) -> activate# XS, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__fst X -> fst# X) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__snd X -> snd# X) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__tail X -> tail# X) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__head X -> head# X) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isPLNat# n__splitAt(V1, V2) -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__fst X -> fst# X) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__snd X -> snd# X) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__tail X -> tail# X) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__head X -> head# X) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isNatural# n__sel(V1, V2) -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isNatural# n__head V1 -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isNatural# n__head V1 -> activate# V1, activate# n__nil() -> nil#()) (isNatural# n__head V1 -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isNatural# n__head V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatural# n__head V1 -> activate# V1, activate# n__fst X -> fst# X) (isNatural# n__head V1 -> activate# V1, activate# n__snd X -> snd# X) (isNatural# n__head V1 -> activate# V1, activate# n__tail X -> tail# X) (isNatural# n__head V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatural# n__head V1 -> activate# V1, activate# n__0() -> 0#()) (isNatural# n__head V1 -> activate# V1, activate# n__head X -> head# X) (isNatural# n__head V1 -> activate# V1, activate# n__s X -> s# X) (isNatural# n__head V1 -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isNatural# n__head V1 -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isNatural# n__head V1 -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__tail V1 -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__tail V1 -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__tail V1 -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__tail V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__tail V1 -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__tail V1 -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__tail V1 -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__tail V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__tail V1 -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__tail V1 -> activate# V1, activate# n__head X -> head# X) (isLNat# n__tail V1 -> activate# V1, activate# n__s X -> s# X) (isLNat# n__tail V1 -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__tail V1 -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__tail V1 -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__fst V1 -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__fst V1 -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__fst V1 -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__fst V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__fst V1 -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__fst V1 -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__fst V1 -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__fst V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__fst V1 -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__fst V1 -> activate# V1, activate# n__head X -> head# X) (isLNat# n__fst V1 -> activate# V1, activate# n__s X -> s# X) (isLNat# n__fst V1 -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__fst V1 -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__fst V1 -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__fst X -> fst# X) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__snd X -> snd# X) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__tail X -> tail# X) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__head X -> head# X) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V1, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__fst X -> fst# X) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__snd X -> snd# X) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__tail X -> tail# X) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__head X -> head# X) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isPLNat# n__pair(V1, V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (U41#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U41#(tt(), V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__fst X -> fst# X) (U41#(tt(), V2) -> activate# V2, activate# n__snd X -> snd# X) (U41#(tt(), V2) -> activate# V2, activate# n__tail X -> tail# X) (U41#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U41#(tt(), V2) -> activate# V2, activate# n__head X -> head# X) (U41#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U41#(tt(), V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U151#(tt(), V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (U151#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U151#(tt(), V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U151#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U151#(tt(), V2) -> activate# V2, activate# n__fst X -> fst# X) (U151#(tt(), V2) -> activate# V2, activate# n__snd X -> snd# X) (U151#(tt(), V2) -> activate# V2, activate# n__tail X -> tail# X) (U151#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U151#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U151#(tt(), V2) -> activate# V2, activate# n__head X -> head# X) (U151#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U151#(tt(), V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U151#(tt(), V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U151#(tt(), V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (U131#(tt(), V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (U131#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U131#(tt(), V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (U131#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U131#(tt(), V2) -> activate# V2, activate# n__fst X -> fst# X) (U131#(tt(), V2) -> activate# V2, activate# n__snd X -> snd# X) (U131#(tt(), V2) -> activate# V2, activate# n__tail X -> tail# X) (U131#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U131#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U131#(tt(), V2) -> activate# V2, activate# n__head X -> head# X) (U131#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U131#(tt(), V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (U131#(tt(), V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (U131#(tt(), V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__fst X -> fst# X) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__snd X -> snd# X) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__tail X -> tail# X) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__head X -> head# X) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__take(V1, V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__natsFrom X -> natsFrom# X) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__fst X -> fst# X) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__snd X -> snd# X) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__tail X -> tail# X) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__head X -> head# X) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__sel(X1, X2) -> sel#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__pair(X1, X2) -> pair#(X1, X2)) (isLNat# n__afterNth(V1, V2) -> activate# V2, activate# n__splitAt(X1, X2) -> splitAt#(X1, X2)) } STATUS: arrows: 0.938613 SCCS (1): Scc: { isLNat# n__natsFrom V1 -> activate# V1, isLNat# n__natsFrom V1 -> isNatural# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V2, isLNat# n__afterNth(V1, V2) -> activate# V1, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2), isLNat# n__cons(V1, V2) -> activate# V2, isLNat# n__cons(V1, V2) -> activate# V1, isLNat# n__cons(V1, V2) -> isNatural# activate V1, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2), isLNat# n__fst V1 -> activate# V1, isLNat# n__fst V1 -> isPLNat# activate V1, isLNat# n__snd V1 -> activate# V1, isLNat# n__snd V1 -> isPLNat# activate V1, isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__tail V1 -> activate# V1, isLNat# n__take(V1, V2) -> activate# V2, isLNat# n__take(V1, V2) -> activate# V1, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2), isLNat# n__take(V1, V2) -> isNatural# activate V1, activate# n__natsFrom X -> natsFrom# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2), activate# n__fst X -> fst# X, activate# n__snd X -> snd# X, activate# n__tail X -> tail# X, activate# n__take(X1, X2) -> take#(X1, X2), activate# n__head X -> head# X, activate# n__sel(X1, X2) -> sel#(X1, X2), activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), U101#(tt(), V2) -> isLNat# activate V2, U101#(tt(), V2) -> activate# V2, U12#(tt(), N, XS) -> activate# XS, U12#(tt(), N, XS) -> activate# N, U12#(tt(), N, XS) -> snd# splitAt(activate N, activate XS), U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), U11#(tt(), N, XS) -> isLNat# activate XS, U11#(tt(), N, XS) -> activate# XS, U11#(tt(), N, XS) -> activate# N, U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), snd# pair(X, Y) -> isLNat# X, snd# pair(X, Y) -> U181#(isLNat X, Y), splitAt#(s N, cons(X, XS)) -> activate# XS, splitAt#(s N, cons(X, XS)) -> isNatural# N, splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), splitAt#(0(), XS) -> isLNat# XS, splitAt#(0(), XS) -> U191#(isLNat XS, XS), U131#(tt(), V2) -> isLNat# activate V2, U131#(tt(), V2) -> activate# V2, U141#(tt(), V2) -> isLNat# activate V2, U141#(tt(), V2) -> activate# V2, U151#(tt(), V2) -> isLNat# activate V2, U151#(tt(), V2) -> activate# V2, U161#(tt(), N) -> activate# N, U172#(tt(), N, XS) -> activate# XS, U172#(tt(), N, XS) -> activate# N, U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS), U172#(tt(), N, XS) -> afterNth#(activate N, activate XS), U171#(tt(), N, XS) -> isLNat# activate XS, U171#(tt(), N, XS) -> activate# XS, U171#(tt(), N, XS) -> activate# N, U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), head# cons(N, XS) -> activate# XS, head# cons(N, XS) -> isNatural# N, head# cons(N, XS) -> U31#(isNatural N, N, activate XS), afterNth#(N, XS) -> U11#(isNatural N, N, XS), afterNth#(N, XS) -> isNatural# N, U182#(tt(), Y) -> activate# Y, U181#(tt(), Y) -> isLNat# activate Y, U181#(tt(), Y) -> activate# Y, U181#(tt(), Y) -> U182#(isLNat activate Y, activate Y), U191#(tt(), XS) -> activate# XS, U202#(tt(), N, X, XS) -> isLNat# activate XS, U202#(tt(), N, X, XS) -> activate# XS, U202#(tt(), N, X, XS) -> activate# N, U202#(tt(), N, X, XS) -> activate# X, U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), isNatural# n__head V1 -> isLNat# activate V1, isNatural# n__head V1 -> activate# V1, isNatural# n__s V1 -> activate# V1, isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2, isNatural# n__sel(V1, V2) -> activate# V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2), isNatural# n__sel(V1, V2) -> isNatural# activate V1, U201#(tt(), N, X, XS) -> activate# XS, U201#(tt(), N, X, XS) -> activate# N, U201#(tt(), N, X, XS) -> activate# X, U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U201#(tt(), N, X, XS) -> isNatural# activate X, U203#(tt(), N, X, XS) -> activate# XS, U203#(tt(), N, X, XS) -> activate# N, U203#(tt(), N, X, XS) -> activate# X, U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), U203#(tt(), N, X, XS) -> U204#(splitAt(activate N, activate XS), activate X), U204#(pair(YS, ZS), X) -> activate# X, U22#(tt(), X) -> activate# X, U21#(tt(), X, Y) -> isLNat# activate Y, U21#(tt(), X, Y) -> activate# Y, U21#(tt(), X, Y) -> activate# X, U21#(tt(), X, Y) -> U22#(isLNat activate Y, activate X), U212#(tt(), XS) -> activate# XS, U211#(tt(), XS) -> isLNat# activate XS, U211#(tt(), XS) -> activate# XS, U211#(tt(), XS) -> U212#(isLNat activate XS, activate XS), U222#(tt(), N, XS) -> activate# XS, U222#(tt(), N, XS) -> activate# N, U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), U222#(tt(), N, XS) -> fst# splitAt(activate N, activate XS), U221#(tt(), N, XS) -> isLNat# activate XS, U221#(tt(), N, XS) -> activate# XS, U221#(tt(), N, XS) -> activate# N, U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), fst# pair(X, Y) -> isLNat# X, fst# pair(X, Y) -> U21#(isLNat X, X, Y), U32#(tt(), N) -> activate# N, U31#(tt(), N, XS) -> isLNat# activate XS, U31#(tt(), N, XS) -> activate# XS, U31#(tt(), N, XS) -> activate# N, U31#(tt(), N, XS) -> U32#(isLNat activate XS, activate N), U41#(tt(), V2) -> isLNat# activate V2, U41#(tt(), V2) -> activate# V2, U51#(tt(), V2) -> isLNat# activate V2, U51#(tt(), V2) -> activate# V2, isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V2, isPLNat# n__pair(V1, V2) -> activate# V1, isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2), isPLNat# n__splitAt(V1, V2) -> activate# V2, isPLNat# n__splitAt(V1, V2) -> activate# V1, isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2), isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, natsFrom# N -> U161#(isNatural N, N), natsFrom# N -> isNatural# N, sel#(N, XS) -> U171#(isNatural N, N, XS), sel#(N, XS) -> isNatural# N, tail# cons(N, XS) -> activate# XS, tail# cons(N, XS) -> isNatural# N, tail# cons(N, XS) -> U211#(isNatural N, activate XS), take#(N, XS) -> isNatural# N, take#(N, XS) -> U221#(isNatural N, N, XS)} SCC (140): Strict: { isLNat# n__natsFrom V1 -> activate# V1, isLNat# n__natsFrom V1 -> isNatural# activate V1, isLNat# n__afterNth(V1, V2) -> activate# V2, isLNat# n__afterNth(V1, V2) -> activate# V1, isLNat# n__afterNth(V1, V2) -> isNatural# activate V1, isLNat# n__afterNth(V1, V2) -> U41#(isNatural activate V1, activate V2), isLNat# n__cons(V1, V2) -> activate# V2, isLNat# n__cons(V1, V2) -> activate# V1, isLNat# n__cons(V1, V2) -> isNatural# activate V1, isLNat# n__cons(V1, V2) -> U51#(isNatural activate V1, activate V2), isLNat# n__fst V1 -> activate# V1, isLNat# n__fst V1 -> isPLNat# activate V1, isLNat# n__snd V1 -> activate# V1, isLNat# n__snd V1 -> isPLNat# activate V1, isLNat# n__tail V1 -> isLNat# activate V1, isLNat# n__tail V1 -> activate# V1, isLNat# n__take(V1, V2) -> activate# V2, isLNat# n__take(V1, V2) -> activate# V1, isLNat# n__take(V1, V2) -> U101#(isNatural activate V1, activate V2), isLNat# n__take(V1, V2) -> isNatural# activate V1, activate# n__natsFrom X -> natsFrom# X, activate# n__afterNth(X1, X2) -> afterNth#(X1, X2), activate# n__fst X -> fst# X, activate# n__snd X -> snd# X, activate# n__tail X -> tail# X, activate# n__take(X1, X2) -> take#(X1, X2), activate# n__head X -> head# X, activate# n__sel(X1, X2) -> sel#(X1, X2), activate# n__splitAt(X1, X2) -> splitAt#(X1, X2), U101#(tt(), V2) -> isLNat# activate V2, U101#(tt(), V2) -> activate# V2, U12#(tt(), N, XS) -> activate# XS, U12#(tt(), N, XS) -> activate# N, U12#(tt(), N, XS) -> snd# splitAt(activate N, activate XS), U12#(tt(), N, XS) -> splitAt#(activate N, activate XS), U11#(tt(), N, XS) -> isLNat# activate XS, U11#(tt(), N, XS) -> activate# XS, U11#(tt(), N, XS) -> activate# N, U11#(tt(), N, XS) -> U12#(isLNat activate XS, activate N, activate XS), snd# pair(X, Y) -> isLNat# X, snd# pair(X, Y) -> U181#(isLNat X, Y), splitAt#(s N, cons(X, XS)) -> activate# XS, splitAt#(s N, cons(X, XS)) -> isNatural# N, splitAt#(s N, cons(X, XS)) -> U201#(isNatural N, N, X, activate XS), splitAt#(0(), XS) -> isLNat# XS, splitAt#(0(), XS) -> U191#(isLNat XS, XS), U131#(tt(), V2) -> isLNat# activate V2, U131#(tt(), V2) -> activate# V2, U141#(tt(), V2) -> isLNat# activate V2, U141#(tt(), V2) -> activate# V2, U151#(tt(), V2) -> isLNat# activate V2, U151#(tt(), V2) -> activate# V2, U161#(tt(), N) -> activate# N, U172#(tt(), N, XS) -> activate# XS, U172#(tt(), N, XS) -> activate# N, U172#(tt(), N, XS) -> head# afterNth(activate N, activate XS), U172#(tt(), N, XS) -> afterNth#(activate N, activate XS), U171#(tt(), N, XS) -> isLNat# activate XS, U171#(tt(), N, XS) -> activate# XS, U171#(tt(), N, XS) -> activate# N, U171#(tt(), N, XS) -> U172#(isLNat activate XS, activate N, activate XS), head# cons(N, XS) -> activate# XS, head# cons(N, XS) -> isNatural# N, head# cons(N, XS) -> U31#(isNatural N, N, activate XS), afterNth#(N, XS) -> U11#(isNatural N, N, XS), afterNth#(N, XS) -> isNatural# N, U182#(tt(), Y) -> activate# Y, U181#(tt(), Y) -> isLNat# activate Y, U181#(tt(), Y) -> activate# Y, U181#(tt(), Y) -> U182#(isLNat activate Y, activate Y), U191#(tt(), XS) -> activate# XS, U202#(tt(), N, X, XS) -> isLNat# activate XS, U202#(tt(), N, X, XS) -> activate# XS, U202#(tt(), N, X, XS) -> activate# N, U202#(tt(), N, X, XS) -> activate# X, U202#(tt(), N, X, XS) -> U203#(isLNat activate XS, activate N, activate X, activate XS), isNatural# n__head V1 -> isLNat# activate V1, isNatural# n__head V1 -> activate# V1, isNatural# n__s V1 -> activate# V1, isNatural# n__s V1 -> isNatural# activate V1, isNatural# n__sel(V1, V2) -> activate# V2, isNatural# n__sel(V1, V2) -> activate# V1, isNatural# n__sel(V1, V2) -> U131#(isNatural activate V1, activate V2), isNatural# n__sel(V1, V2) -> isNatural# activate V1, U201#(tt(), N, X, XS) -> activate# XS, U201#(tt(), N, X, XS) -> activate# N, U201#(tt(), N, X, XS) -> activate# X, U201#(tt(), N, X, XS) -> U202#(isNatural activate X, activate N, activate X, activate XS), U201#(tt(), N, X, XS) -> isNatural# activate X, U203#(tt(), N, X, XS) -> activate# XS, U203#(tt(), N, X, XS) -> activate# N, U203#(tt(), N, X, XS) -> activate# X, U203#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), U203#(tt(), N, X, XS) -> U204#(splitAt(activate N, activate XS), activate X), U204#(pair(YS, ZS), X) -> activate# X, U22#(tt(), X) -> activate# X, U21#(tt(), X, Y) -> isLNat# activate Y, U21#(tt(), X, Y) -> activate# Y, U21#(tt(), X, Y) -> activate# X, U21#(tt(), X, Y) -> U22#(isLNat activate Y, activate X), U212#(tt(), XS) -> activate# XS, U211#(tt(), XS) -> isLNat# activate XS, U211#(tt(), XS) -> activate# XS, U211#(tt(), XS) -> U212#(isLNat activate XS, activate XS), U222#(tt(), N, XS) -> activate# XS, U222#(tt(), N, XS) -> activate# N, U222#(tt(), N, XS) -> splitAt#(activate N, activate XS), U222#(tt(), N, XS) -> fst# splitAt(activate N, activate XS), U221#(tt(), N, XS) -> isLNat# activate XS, U221#(tt(), N, XS) -> activate# XS, U221#(tt(), N, XS) -> activate# N, U221#(tt(), N, XS) -> U222#(isLNat activate XS, activate N, activate XS), fst# pair(X, Y) -> isLNat# X, fst# pair(X, Y) -> U21#(isLNat X, X, Y), U32#(tt(), N) -> activate# N, U31#(tt(), N, XS) -> isLNat# activate XS, U31#(tt(), N, XS) -> activate# XS, U31#(tt(), N, XS) -> activate# N, U31#(tt(), N, XS) -> U32#(isLNat activate XS, activate N), U41#(tt(), V2) -> isLNat# activate V2, U41#(tt(), V2) -> activate# V2, U51#(tt(), V2) -> isLNat# activate V2, U51#(tt(), V2) -> activate# V2, isPLNat# n__pair(V1, V2) -> isLNat# activate V1, isPLNat# n__pair(V1, V2) -> activate# V2, isPLNat# n__pair(V1, V2) -> activate# V1, isPLNat# n__pair(V1, V2) -> U141#(isLNat activate V1, activate V2), isPLNat# n__splitAt(V1, V2) -> activate# V2, isPLNat# n__splitAt(V1, V2) -> activate# V1, isPLNat# n__splitAt(V1, V2) -> U151#(isNatural activate V1, activate V2), isPLNat# n__splitAt(V1, V2) -> isNatural# activate V1, natsFrom# N -> U161#(isNatural N, N), natsFrom# N -> isNatural# N, sel#(N, XS) -> U171#(isNatural N, N, XS), sel#(N, XS) -> isNatural# N, tail# cons(N, XS) -> activate# XS, tail# cons(N, XS) -> isNatural# N, tail# cons(N, XS) -> U211#(isNatural N, activate XS), take#(N, XS) -> isNatural# N, take#(N, XS) -> U221#(isNatural N, N, XS)} Weak: { U102 tt() -> tt(), isLNat n__natsFrom V1 -> U71 isNatural activate V1, 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__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), activate X -> X, activate n__natsFrom X -> natsFrom X, activate n__nil() -> nil(), activate n__afterNth(X1, X2) -> afterNth(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__fst X -> fst X, activate n__snd X -> snd X, activate n__tail X -> tail X, activate n__take(X1, X2) -> take(X1, X2), activate n__0() -> 0(), activate n__head X -> head X, activate n__s X -> s X, activate n__sel(X1, X2) -> sel(X1, X2), activate n__pair(X1, X2) -> pair(X1, X2), activate n__splitAt(X1, X2) -> splitAt(X1, X2), U101(tt(), V2) -> U102 isLNat activate V2, U12(tt(), N, XS) -> snd splitAt(activate N, activate XS), U11(tt(), N, XS) -> U12(isLNat activate XS, activate N, activate XS), U111 tt() -> tt(), snd X -> n__snd X, snd pair(X, Y) -> U181(isLNat X, Y), splitAt(X1, X2) -> n__splitAt(X1, X2), splitAt(s N, cons(X, XS)) -> U201(isNatural N, N, X, activate XS), splitAt(0(), XS) -> U191(isLNat XS, XS), U121 tt() -> tt(), U132 tt() -> tt(), U131(tt(), V2) -> U132 isLNat activate V2, U142 tt() -> tt(), U141(tt(), V2) -> U142 isLNat activate V2, U152 tt() -> tt(), U151(tt(), V2) -> U152 isLNat activate V2, cons(X1, X2) -> n__cons(X1, X2), s X -> n__s X, U161(tt(), N) -> cons(activate N, n__natsFrom s activate N), U172(tt(), N, XS) -> head afterNth(activate N, activate XS), U171(tt(), N, XS) -> U172(isLNat activate XS, activate N, activate XS), head X -> n__head X, head cons(N, XS) -> U31(isNatural N, N, activate XS), afterNth(N, XS) -> U11(isNatural N, N, XS), afterNth(X1, X2) -> n__afterNth(X1, X2), U182(tt(), Y) -> activate Y, U181(tt(), Y) -> U182(isLNat activate Y, activate Y), pair(X1, X2) -> n__pair(X1, X2), nil() -> n__nil(), U191(tt(), XS) -> pair(nil(), activate XS), U202(tt(), N, X, XS) -> U203(isLNat activate XS, activate N, activate X, activate XS), 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), U201(tt(), N, X, XS) -> U202(isNatural activate X, 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), U22(tt(), X) -> activate X, U21(tt(), X, Y) -> U22(isLNat activate Y, activate X), U212(tt(), XS) -> activate XS, U211(tt(), XS) -> U212(isLNat activate XS, activate XS), U222(tt(), N, XS) -> fst splitAt(activate N, activate XS), U221(tt(), N, XS) -> U222(isLNat activate XS, activate N, activate XS), fst X -> n__fst X, fst pair(X, Y) -> U21(isLNat X, X, Y), U32(tt(), N) -> activate N, U31(tt(), N, XS) -> U32(isLNat activate XS, activate N), U42 tt() -> tt(), U41(tt(), V2) -> U42 isLNat activate V2, U52 tt() -> tt(), U51(tt(), V2) -> U52 isLNat activate V2, U61 tt() -> tt(), U71 tt() -> tt(), U81 tt() -> tt(), U91 tt() -> tt(), 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), natsFrom X -> n__natsFrom X, sel(N, XS) -> U171(isNatural N, N, XS), sel(X1, X2) -> n__sel(X1, X2), 0() -> n__0(), tail X -> n__tail X, tail cons(N, XS) -> U211(isNatural N, activate XS), take(N, XS) -> U221(isNatural N, N, XS), take(X1, X2) -> n__take(X1, X2)} Open