MAYBE

Problem:
 U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2))
 U102(tt(),V2) -> U103(isLNat(activate(V2)))
 U103(tt()) -> tt()
 U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
 U111(tt(),V1) -> U112(isLNat(activate(V1)))
 U112(tt()) -> tt()
 U121(tt(),V1) -> U122(isNatural(activate(V1)))
 U122(tt()) -> tt()
 U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2))
 U132(tt(),V2) -> U133(isLNat(activate(V2)))
 U133(tt()) -> tt()
 U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2))
 U142(tt(),V2) -> U143(isLNat(activate(V2)))
 U143(tt()) -> tt()
 U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2))
 U152(tt(),V2) -> U153(isLNat(activate(V2)))
 U153(tt()) -> tt()
 U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N))))
 U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
 U181(tt(),Y) -> activate(Y)
 U191(tt(),XS) -> pair(nil(),activate(XS))
 U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X))
 U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
 U21(tt(),X) -> activate(X)
 U211(tt(),XS) -> activate(XS)
 U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
 U31(tt(),N) -> activate(N)
 U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2))
 U42(tt(),V2) -> U43(isLNat(activate(V2)))
 U43(tt()) -> tt()
 U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2))
 U52(tt(),V2) -> U53(isLNat(activate(V2)))
 U53(tt()) -> tt()
 U61(tt(),V1) -> U62(isPLNat(activate(V1)))
 U62(tt()) -> tt()
 U71(tt(),V1) -> U72(isNatural(activate(V1)))
 U72(tt()) -> tt()
 U81(tt(),V1) -> U82(isPLNat(activate(V1)))
 U82(tt()) -> tt()
 U91(tt(),V1) -> U92(isLNat(activate(V1)))
 U92(tt()) -> tt()
 afterNth(N,XS) ->
 U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
 and(tt(),X) -> activate(X)
 fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
 head(cons(N,XS)) ->
 U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                      n__isLNatKind(activate(XS)))),
     N)
 isLNat(n__nil()) -> tt()
 isLNat(n__afterNth(V1,V2)) ->
 U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
 isLNat(n__cons(V1,V2)) ->
 U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
 isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1))
 isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1))
 isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1))
 isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1))
 isLNat(n__take(V1,V2)) ->
 U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
 isLNatKind(n__nil()) -> tt()
 isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
 isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
 isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
 isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
 isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
 isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
 isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
 isNatural(n__0()) -> tt()
 isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1))
 isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1))
 isNatural(n__sel(V1,V2)) ->
 U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
 isNaturalKind(n__0()) -> tt()
 isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
 isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
 isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
 isPLNat(n__pair(V1,V2)) ->
 U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
 isPLNat(n__splitAt(V1,V2)) ->
 U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
 isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
 isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
 natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N)
 sel(N,XS) ->
 U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
 snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
 splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS)
 splitAt(s(N),cons(X,XS)) ->
 U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                       n__and(isLNat(activate(XS)),
                                                              n__isLNatKind
                                                              (activate(XS))))),
      N,X,activate(XS))
 tail(cons(N,XS)) ->
 U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                       n__isLNatKind(activate(XS)))),
      activate(XS))
 take(N,XS) ->
 U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
 natsFrom(X) -> n__natsFrom(X)
 isNaturalKind(X) -> n__isNaturalKind(X)
 and(X1,X2) -> n__and(X1,X2)
 isLNatKind(X) -> n__isLNatKind(X)
 nil() -> n__nil()
 afterNth(X1,X2) -> n__afterNth(X1,X2)
 cons(X1,X2) -> n__cons(X1,X2)
 fst(X) -> n__fst(X)
 snd(X) -> n__snd(X)
 tail(X) -> n__tail(X)
 take(X1,X2) -> n__take(X1,X2)
 0() -> n__0()
 head(X) -> n__head(X)
 s(X) -> n__s(X)
 sel(X1,X2) -> n__sel(X1,X2)
 pair(X1,X2) -> n__pair(X1,X2)
 splitAt(X1,X2) -> n__splitAt(X1,X2)
 activate(n__natsFrom(X)) -> natsFrom(X)
 activate(n__isNaturalKind(X)) -> isNaturalKind(X)
 activate(n__and(X1,X2)) -> and(X1,X2)
 activate(n__isLNatKind(X)) -> isLNatKind(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)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   U101#(tt(),V1,V2) -> activate#(V2)
   U101#(tt(),V1,V2) -> activate#(V1)
   U101#(tt(),V1,V2) -> isNatural#(activate(V1))
   U101#(tt(),V1,V2) -> U102#(isNatural(activate(V1)),activate(V2))
   U102#(tt(),V2) -> activate#(V2)
   U102#(tt(),V2) -> isLNat#(activate(V2))
   U102#(tt(),V2) -> U103#(isLNat(activate(V2)))
   U11#(tt(),N,XS) -> activate#(XS)
   U11#(tt(),N,XS) -> activate#(N)
   U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
   U111#(tt(),V1) -> activate#(V1)
   U111#(tt(),V1) -> isLNat#(activate(V1))
   U111#(tt(),V1) -> U112#(isLNat(activate(V1)))
   U121#(tt(),V1) -> activate#(V1)
   U121#(tt(),V1) -> isNatural#(activate(V1))
   U121#(tt(),V1) -> U122#(isNatural(activate(V1)))
   U131#(tt(),V1,V2) -> activate#(V2)
   U131#(tt(),V1,V2) -> activate#(V1)
   U131#(tt(),V1,V2) -> isNatural#(activate(V1))
   U131#(tt(),V1,V2) -> U132#(isNatural(activate(V1)),activate(V2))
   U132#(tt(),V2) -> activate#(V2)
   U132#(tt(),V2) -> isLNat#(activate(V2))
   U132#(tt(),V2) -> U133#(isLNat(activate(V2)))
   U141#(tt(),V1,V2) -> activate#(V2)
   U141#(tt(),V1,V2) -> activate#(V1)
   U141#(tt(),V1,V2) -> isLNat#(activate(V1))
   U141#(tt(),V1,V2) -> U142#(isLNat(activate(V1)),activate(V2))
   U142#(tt(),V2) -> activate#(V2)
   U142#(tt(),V2) -> isLNat#(activate(V2))
   U142#(tt(),V2) -> U143#(isLNat(activate(V2)))
   U151#(tt(),V1,V2) -> activate#(V2)
   U151#(tt(),V1,V2) -> activate#(V1)
   U151#(tt(),V1,V2) -> isNatural#(activate(V1))
   U151#(tt(),V1,V2) -> U152#(isNatural(activate(V1)),activate(V2))
   U152#(tt(),V2) -> activate#(V2)
   U152#(tt(),V2) -> isLNat#(activate(V2))
   U152#(tt(),V2) -> U153#(isLNat(activate(V2)))
   U161#(tt(),N) -> s#(activate(N))
   U161#(tt(),N) -> activate#(N)
   U161#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N))))
   U171#(tt(),N,XS) -> activate#(XS)
   U171#(tt(),N,XS) -> activate#(N)
   U171#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
   U171#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
   U181#(tt(),Y) -> activate#(Y)
   U191#(tt(),XS) -> activate#(XS)
   U191#(tt(),XS) -> nil#()
   U191#(tt(),XS) -> pair#(nil(),activate(XS))
   U201#(tt(),N,X,XS) -> activate#(X)
   U201#(tt(),N,X,XS) -> activate#(XS)
   U201#(tt(),N,X,XS) -> activate#(N)
   U201#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
   U201#(tt(),N,X,XS) -> U202#(splitAt(activate(N),activate(XS)),activate(X))
   U202#(pair(YS,ZS),X) -> activate#(X)
   U202#(pair(YS,ZS),X) -> cons#(activate(X),YS)
   U202#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS)
   U21#(tt(),X) -> activate#(X)
   U211#(tt(),XS) -> activate#(XS)
   U221#(tt(),N,XS) -> activate#(XS)
   U221#(tt(),N,XS) -> activate#(N)
   U221#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U221#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
   U31#(tt(),N) -> activate#(N)
   U41#(tt(),V1,V2) -> activate#(V2)
   U41#(tt(),V1,V2) -> activate#(V1)
   U41#(tt(),V1,V2) -> isNatural#(activate(V1))
   U41#(tt(),V1,V2) -> U42#(isNatural(activate(V1)),activate(V2))
   U42#(tt(),V2) -> activate#(V2)
   U42#(tt(),V2) -> isLNat#(activate(V2))
   U42#(tt(),V2) -> U43#(isLNat(activate(V2)))
   U51#(tt(),V1,V2) -> activate#(V2)
   U51#(tt(),V1,V2) -> activate#(V1)
   U51#(tt(),V1,V2) -> isNatural#(activate(V1))
   U51#(tt(),V1,V2) -> U52#(isNatural(activate(V1)),activate(V2))
   U52#(tt(),V2) -> activate#(V2)
   U52#(tt(),V2) -> isLNat#(activate(V2))
   U52#(tt(),V2) -> U53#(isLNat(activate(V2)))
   U61#(tt(),V1) -> activate#(V1)
   U61#(tt(),V1) -> isPLNat#(activate(V1))
   U61#(tt(),V1) -> U62#(isPLNat(activate(V1)))
   U71#(tt(),V1) -> activate#(V1)
   U71#(tt(),V1) -> isNatural#(activate(V1))
   U71#(tt(),V1) -> U72#(isNatural(activate(V1)))
   U81#(tt(),V1) -> activate#(V1)
   U81#(tt(),V1) -> isPLNat#(activate(V1))
   U81#(tt(),V1) -> U82#(isPLNat(activate(V1)))
   U91#(tt(),V1) -> activate#(V1)
   U91#(tt(),V1) -> isLNat#(activate(V1))
   U91#(tt(),V1) -> U92#(isLNat(activate(V1)))
   afterNth#(N,XS) -> isLNat#(XS)
   afterNth#(N,XS) -> isNatural#(N)
   afterNth#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
   afterNth#(N,XS) ->
   and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
   afterNth#(N,XS) ->
   U11#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   and#(tt(),X) -> activate#(X)
   fst#(pair(X,Y)) -> isLNat#(Y)
   fst#(pair(X,Y)) -> isLNat#(X)
   fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X))
   fst#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
   fst#(pair(X,Y)) ->
   U21#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
   head#(cons(N,XS)) -> activate#(XS)
   head#(cons(N,XS)) -> isLNat#(activate(XS))
   head#(cons(N,XS)) -> isNatural#(N)
   head#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
   head#(cons(N,XS)) ->
   and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                     n__isLNatKind(activate(XS))))
   head#(cons(N,XS)) ->
   U31#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                         n__isLNatKind
                                                         (activate(XS)))),
        N)
   isLNat#(n__afterNth(V1,V2)) -> activate#(V2)
   isLNat#(n__afterNth(V1,V2)) -> activate#(V1)
   isLNat#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1))
   isLNat#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNat#(n__afterNth(V1,V2)) ->
   U41#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isLNat#(n__cons(V1,V2)) -> activate#(V2)
   isLNat#(n__cons(V1,V2)) -> activate#(V1)
   isLNat#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1))
   isLNat#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNat#(n__cons(V1,V2)) ->
   U51#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isLNat#(n__fst(V1)) -> activate#(V1)
   isLNat#(n__fst(V1)) -> isPLNatKind#(activate(V1))
   isLNat#(n__fst(V1)) -> U61#(isPLNatKind(activate(V1)),activate(V1))
   isLNat#(n__natsFrom(V1)) -> activate#(V1)
   isLNat#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1))
   isLNat#(n__natsFrom(V1)) -> U71#(isNaturalKind(activate(V1)),activate(V1))
   isLNat#(n__snd(V1)) -> activate#(V1)
   isLNat#(n__snd(V1)) -> isPLNatKind#(activate(V1))
   isLNat#(n__snd(V1)) -> U81#(isPLNatKind(activate(V1)),activate(V1))
   isLNat#(n__tail(V1)) -> activate#(V1)
   isLNat#(n__tail(V1)) -> isLNatKind#(activate(V1))
   isLNat#(n__tail(V1)) -> U91#(isLNatKind(activate(V1)),activate(V1))
   isLNat#(n__take(V1,V2)) -> activate#(V2)
   isLNat#(n__take(V1,V2)) -> activate#(V1)
   isLNat#(n__take(V1,V2)) -> isNaturalKind#(activate(V1))
   isLNat#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNat#(n__take(V1,V2)) ->
   U101#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isLNatKind#(n__afterNth(V1,V2)) -> activate#(V2)
   isLNatKind#(n__afterNth(V1,V2)) -> activate#(V1)
   isLNatKind#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1))
   isLNatKind#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNatKind#(n__cons(V1,V2)) -> activate#(V2)
   isLNatKind#(n__cons(V1,V2)) -> activate#(V1)
   isLNatKind#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1))
   isLNatKind#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNatKind#(n__fst(V1)) -> activate#(V1)
   isLNatKind#(n__fst(V1)) -> isPLNatKind#(activate(V1))
   isLNatKind#(n__natsFrom(V1)) -> activate#(V1)
   isLNatKind#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1))
   isLNatKind#(n__snd(V1)) -> activate#(V1)
   isLNatKind#(n__snd(V1)) -> isPLNatKind#(activate(V1))
   isLNatKind#(n__tail(V1)) -> activate#(V1)
   isLNatKind#(n__tail(V1)) -> isLNatKind#(activate(V1))
   isLNatKind#(n__take(V1,V2)) -> activate#(V2)
   isLNatKind#(n__take(V1,V2)) -> activate#(V1)
   isLNatKind#(n__take(V1,V2)) -> isNaturalKind#(activate(V1))
   isLNatKind#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isNatural#(n__head(V1)) -> activate#(V1)
   isNatural#(n__head(V1)) -> isLNatKind#(activate(V1))
   isNatural#(n__head(V1)) -> U111#(isLNatKind(activate(V1)),activate(V1))
   isNatural#(n__s(V1)) -> activate#(V1)
   isNatural#(n__s(V1)) -> isNaturalKind#(activate(V1))
   isNatural#(n__s(V1)) -> U121#(isNaturalKind(activate(V1)),activate(V1))
   isNatural#(n__sel(V1,V2)) -> activate#(V2)
   isNatural#(n__sel(V1,V2)) -> activate#(V1)
   isNatural#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1))
   isNatural#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isNatural#(n__sel(V1,V2)) ->
   U131#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isNaturalKind#(n__head(V1)) -> activate#(V1)
   isNaturalKind#(n__head(V1)) -> isLNatKind#(activate(V1))
   isNaturalKind#(n__s(V1)) -> activate#(V1)
   isNaturalKind#(n__s(V1)) -> isNaturalKind#(activate(V1))
   isNaturalKind#(n__sel(V1,V2)) -> activate#(V2)
   isNaturalKind#(n__sel(V1,V2)) -> activate#(V1)
   isNaturalKind#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1))
   isNaturalKind#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isPLNat#(n__pair(V1,V2)) -> activate#(V2)
   isPLNat#(n__pair(V1,V2)) -> activate#(V1)
   isPLNat#(n__pair(V1,V2)) -> isLNatKind#(activate(V1))
   isPLNat#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
   isPLNat#(n__pair(V1,V2)) ->
   U141#(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isPLNat#(n__splitAt(V1,V2)) -> activate#(V2)
   isPLNat#(n__splitAt(V1,V2)) -> activate#(V1)
   isPLNat#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1))
   isPLNat#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isPLNat#(n__splitAt(V1,V2)) ->
   U151#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isPLNatKind#(n__pair(V1,V2)) -> activate#(V2)
   isPLNatKind#(n__pair(V1,V2)) -> activate#(V1)
   isPLNatKind#(n__pair(V1,V2)) -> isLNatKind#(activate(V1))
   isPLNatKind#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
   isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V2)
   isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V1)
   isPLNatKind#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1))
   isPLNatKind#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   natsFrom#(N) -> isNatural#(N)
   natsFrom#(N) -> and#(isNatural(N),n__isNaturalKind(N))
   natsFrom#(N) -> U161#(and(isNatural(N),n__isNaturalKind(N)),N)
   sel#(N,XS) -> isLNat#(XS)
   sel#(N,XS) -> isNatural#(N)
   sel#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
   sel#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
   sel#(N,XS) ->
   U171#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   snd#(pair(X,Y)) -> isLNat#(Y)
   snd#(pair(X,Y)) -> isLNat#(X)
   snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X))
   snd#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
   snd#(pair(X,Y)) ->
   U181#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
   splitAt#(0(),XS) -> isLNat#(XS)
   splitAt#(0(),XS) -> and#(isLNat(XS),n__isLNatKind(XS))
   splitAt#(0(),XS) -> U191#(and(isLNat(XS),n__isLNatKind(XS)),XS)
   splitAt#(s(N),cons(X,XS)) -> activate#(XS)
   splitAt#(s(N),cons(X,XS)) -> isLNat#(activate(XS))
   splitAt#(s(N),cons(X,XS)) -> isNatural#(X)
   splitAt#(s(N),cons(X,XS)) -> and#(isNatural(X),n__isNaturalKind(X))
   splitAt#(s(N),cons(X,XS)) -> isNatural#(N)
   splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
   splitAt#(s(N),cons(X,XS)) ->
   and#(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                     n__and(isLNat(activate(XS)),
                                                            n__isLNatKind
                                                            (activate(XS)))))
   splitAt#(s(N),cons(X,XS)) ->
   U201#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                          n__and(isLNat(activate(XS)),
                                                                 n__isLNatKind
                                                                 (activate(XS))))),
         N,X,activate(XS))
   tail#(cons(N,XS)) -> activate#(XS)
   tail#(cons(N,XS)) -> isLNat#(activate(XS))
   tail#(cons(N,XS)) -> isNatural#(N)
   tail#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
   tail#(cons(N,XS)) ->
   and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                     n__isLNatKind(activate(XS))))
   tail#(cons(N,XS)) ->
   U211#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                          n__isLNatKind
                                                          (activate(XS)))),
         activate(XS))
   take#(N,XS) -> isLNat#(XS)
   take#(N,XS) -> isNatural#(N)
   take#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
   take#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
   take#(N,XS) ->
   U221#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   activate#(n__natsFrom(X)) -> natsFrom#(X)
   activate#(n__isNaturalKind(X)) -> isNaturalKind#(X)
   activate#(n__and(X1,X2)) -> and#(X1,X2)
   activate#(n__isLNatKind(X)) -> isLNatKind#(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)
  TRS:
   U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2))
   U102(tt(),V2) -> U103(isLNat(activate(V2)))
   U103(tt()) -> tt()
   U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
   U111(tt(),V1) -> U112(isLNat(activate(V1)))
   U112(tt()) -> tt()
   U121(tt(),V1) -> U122(isNatural(activate(V1)))
   U122(tt()) -> tt()
   U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2))
   U132(tt(),V2) -> U133(isLNat(activate(V2)))
   U133(tt()) -> tt()
   U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2))
   U142(tt(),V2) -> U143(isLNat(activate(V2)))
   U143(tt()) -> tt()
   U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2))
   U152(tt(),V2) -> U153(isLNat(activate(V2)))
   U153(tt()) -> tt()
   U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N))))
   U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
   U181(tt(),Y) -> activate(Y)
   U191(tt(),XS) -> pair(nil(),activate(XS))
   U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X))
   U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
   U21(tt(),X) -> activate(X)
   U211(tt(),XS) -> activate(XS)
   U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
   U31(tt(),N) -> activate(N)
   U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2))
   U42(tt(),V2) -> U43(isLNat(activate(V2)))
   U43(tt()) -> tt()
   U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2))
   U52(tt(),V2) -> U53(isLNat(activate(V2)))
   U53(tt()) -> tt()
   U61(tt(),V1) -> U62(isPLNat(activate(V1)))
   U62(tt()) -> tt()
   U71(tt(),V1) -> U72(isNatural(activate(V1)))
   U72(tt()) -> tt()
   U81(tt(),V1) -> U82(isPLNat(activate(V1)))
   U82(tt()) -> tt()
   U91(tt(),V1) -> U92(isLNat(activate(V1)))
   U92(tt()) -> tt()
   afterNth(N,XS) ->
   U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   and(tt(),X) -> activate(X)
   fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
   head(cons(N,XS)) ->
   U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                        n__isLNatKind
                                                        (activate(XS)))),
       N)
   isLNat(n__nil()) -> tt()
   isLNat(n__afterNth(V1,V2)) ->
   U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isLNat(n__cons(V1,V2)) ->
   U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1))
   isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1))
   isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1))
   isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1))
   isLNat(n__take(V1,V2)) ->
   U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isLNatKind(n__nil()) -> tt()
   isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
   isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
   isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
   isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
   isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isNatural(n__0()) -> tt()
   isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1))
   isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1))
   isNatural(n__sel(V1,V2)) ->
   U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isNaturalKind(n__0()) -> tt()
   isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
   isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
   isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   isPLNat(n__pair(V1,V2)) ->
   U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isPLNat(n__splitAt(V1,V2)) ->
   U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
   isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N)
   sel(N,XS) ->
   U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   snd(pair(X,Y)) ->
   U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
   splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS)
   splitAt(s(N),cons(X,XS)) ->
   U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                         n__and(isLNat(activate(XS)),
                                                                n__isLNatKind
                                                                (activate(XS))))),
        N,X,activate(XS))
   tail(cons(N,XS)) ->
   U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                         n__isLNatKind
                                                         (activate(XS)))),
        activate(XS))
   take(N,XS) ->
   U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   natsFrom(X) -> n__natsFrom(X)
   isNaturalKind(X) -> n__isNaturalKind(X)
   and(X1,X2) -> n__and(X1,X2)
   isLNatKind(X) -> n__isLNatKind(X)
   nil() -> n__nil()
   afterNth(X1,X2) -> n__afterNth(X1,X2)
   cons(X1,X2) -> n__cons(X1,X2)
   fst(X) -> n__fst(X)
   snd(X) -> n__snd(X)
   tail(X) -> n__tail(X)
   take(X1,X2) -> n__take(X1,X2)
   0() -> n__0()
   head(X) -> n__head(X)
   s(X) -> n__s(X)
   sel(X1,X2) -> n__sel(X1,X2)
   pair(X1,X2) -> n__pair(X1,X2)
   splitAt(X1,X2) -> n__splitAt(X1,X2)
   activate(n__natsFrom(X)) -> natsFrom(X)
   activate(n__isNaturalKind(X)) -> isNaturalKind(X)
   activate(n__and(X1,X2)) -> and(X1,X2)
   activate(n__isLNatKind(X)) -> isLNatKind(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)
   activate(X) -> X
  TDG Processor:
   DPs:
    U101#(tt(),V1,V2) -> activate#(V2)
    U101#(tt(),V1,V2) -> activate#(V1)
    U101#(tt(),V1,V2) -> isNatural#(activate(V1))
    U101#(tt(),V1,V2) -> U102#(isNatural(activate(V1)),activate(V2))
    U102#(tt(),V2) -> activate#(V2)
    U102#(tt(),V2) -> isLNat#(activate(V2))
    U102#(tt(),V2) -> U103#(isLNat(activate(V2)))
    U11#(tt(),N,XS) -> activate#(XS)
    U11#(tt(),N,XS) -> activate#(N)
    U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
    U111#(tt(),V1) -> activate#(V1)
    U111#(tt(),V1) -> isLNat#(activate(V1))
    U111#(tt(),V1) -> U112#(isLNat(activate(V1)))
    U121#(tt(),V1) -> activate#(V1)
    U121#(tt(),V1) -> isNatural#(activate(V1))
    U121#(tt(),V1) -> U122#(isNatural(activate(V1)))
    U131#(tt(),V1,V2) -> activate#(V2)
    U131#(tt(),V1,V2) -> activate#(V1)
    U131#(tt(),V1,V2) -> isNatural#(activate(V1))
    U131#(tt(),V1,V2) -> U132#(isNatural(activate(V1)),activate(V2))
    U132#(tt(),V2) -> activate#(V2)
    U132#(tt(),V2) -> isLNat#(activate(V2))
    U132#(tt(),V2) -> U133#(isLNat(activate(V2)))
    U141#(tt(),V1,V2) -> activate#(V2)
    U141#(tt(),V1,V2) -> activate#(V1)
    U141#(tt(),V1,V2) -> isLNat#(activate(V1))
    U141#(tt(),V1,V2) -> U142#(isLNat(activate(V1)),activate(V2))
    U142#(tt(),V2) -> activate#(V2)
    U142#(tt(),V2) -> isLNat#(activate(V2))
    U142#(tt(),V2) -> U143#(isLNat(activate(V2)))
    U151#(tt(),V1,V2) -> activate#(V2)
    U151#(tt(),V1,V2) -> activate#(V1)
    U151#(tt(),V1,V2) -> isNatural#(activate(V1))
    U151#(tt(),V1,V2) -> U152#(isNatural(activate(V1)),activate(V2))
    U152#(tt(),V2) -> activate#(V2)
    U152#(tt(),V2) -> isLNat#(activate(V2))
    U152#(tt(),V2) -> U153#(isLNat(activate(V2)))
    U161#(tt(),N) -> s#(activate(N))
    U161#(tt(),N) -> activate#(N)
    U161#(tt(),N) -> cons#(activate(N),n__natsFrom(s(activate(N))))
    U171#(tt(),N,XS) -> activate#(XS)
    U171#(tt(),N,XS) -> activate#(N)
    U171#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
    U171#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
    U181#(tt(),Y) -> activate#(Y)
    U191#(tt(),XS) -> activate#(XS)
    U191#(tt(),XS) -> nil#()
    U191#(tt(),XS) -> pair#(nil(),activate(XS))
    U201#(tt(),N,X,XS) -> activate#(X)
    U201#(tt(),N,X,XS) -> activate#(XS)
    U201#(tt(),N,X,XS) -> activate#(N)
    U201#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
    U201#(tt(),N,X,XS) -> U202#(splitAt(activate(N),activate(XS)),activate(X))
    U202#(pair(YS,ZS),X) -> activate#(X)
    U202#(pair(YS,ZS),X) -> cons#(activate(X),YS)
    U202#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS)
    U21#(tt(),X) -> activate#(X)
    U211#(tt(),XS) -> activate#(XS)
    U221#(tt(),N,XS) -> activate#(XS)
    U221#(tt(),N,XS) -> activate#(N)
    U221#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U221#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
    U31#(tt(),N) -> activate#(N)
    U41#(tt(),V1,V2) -> activate#(V2)
    U41#(tt(),V1,V2) -> activate#(V1)
    U41#(tt(),V1,V2) -> isNatural#(activate(V1))
    U41#(tt(),V1,V2) -> U42#(isNatural(activate(V1)),activate(V2))
    U42#(tt(),V2) -> activate#(V2)
    U42#(tt(),V2) -> isLNat#(activate(V2))
    U42#(tt(),V2) -> U43#(isLNat(activate(V2)))
    U51#(tt(),V1,V2) -> activate#(V2)
    U51#(tt(),V1,V2) -> activate#(V1)
    U51#(tt(),V1,V2) -> isNatural#(activate(V1))
    U51#(tt(),V1,V2) -> U52#(isNatural(activate(V1)),activate(V2))
    U52#(tt(),V2) -> activate#(V2)
    U52#(tt(),V2) -> isLNat#(activate(V2))
    U52#(tt(),V2) -> U53#(isLNat(activate(V2)))
    U61#(tt(),V1) -> activate#(V1)
    U61#(tt(),V1) -> isPLNat#(activate(V1))
    U61#(tt(),V1) -> U62#(isPLNat(activate(V1)))
    U71#(tt(),V1) -> activate#(V1)
    U71#(tt(),V1) -> isNatural#(activate(V1))
    U71#(tt(),V1) -> U72#(isNatural(activate(V1)))
    U81#(tt(),V1) -> activate#(V1)
    U81#(tt(),V1) -> isPLNat#(activate(V1))
    U81#(tt(),V1) -> U82#(isPLNat(activate(V1)))
    U91#(tt(),V1) -> activate#(V1)
    U91#(tt(),V1) -> isLNat#(activate(V1))
    U91#(tt(),V1) -> U92#(isLNat(activate(V1)))
    afterNth#(N,XS) -> isLNat#(XS)
    afterNth#(N,XS) -> isNatural#(N)
    afterNth#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
    afterNth#(N,XS) ->
    and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
    afterNth#(N,XS) ->
    U11#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    and#(tt(),X) -> activate#(X)
    fst#(pair(X,Y)) -> isLNat#(Y)
    fst#(pair(X,Y)) -> isLNat#(X)
    fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X))
    fst#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
    fst#(pair(X,Y)) ->
    U21#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
    head#(cons(N,XS)) -> activate#(XS)
    head#(cons(N,XS)) -> isLNat#(activate(XS))
    head#(cons(N,XS)) -> isNatural#(N)
    head#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
    head#(cons(N,XS)) ->
    and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                      n__isLNatKind(activate(XS))))
    head#(cons(N,XS)) ->
    U31#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                          n__isLNatKind
                                                          (activate(XS)))),
         N)
    isLNat#(n__afterNth(V1,V2)) -> activate#(V2)
    isLNat#(n__afterNth(V1,V2)) -> activate#(V1)
    isLNat#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1))
    isLNat#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNat#(n__afterNth(V1,V2)) ->
    U41#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isLNat#(n__cons(V1,V2)) -> activate#(V2)
    isLNat#(n__cons(V1,V2)) -> activate#(V1)
    isLNat#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1))
    isLNat#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNat#(n__cons(V1,V2)) ->
    U51#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isLNat#(n__fst(V1)) -> activate#(V1)
    isLNat#(n__fst(V1)) -> isPLNatKind#(activate(V1))
    isLNat#(n__fst(V1)) -> U61#(isPLNatKind(activate(V1)),activate(V1))
    isLNat#(n__natsFrom(V1)) -> activate#(V1)
    isLNat#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1))
    isLNat#(n__natsFrom(V1)) -> U71#(isNaturalKind(activate(V1)),activate(V1))
    isLNat#(n__snd(V1)) -> activate#(V1)
    isLNat#(n__snd(V1)) -> isPLNatKind#(activate(V1))
    isLNat#(n__snd(V1)) -> U81#(isPLNatKind(activate(V1)),activate(V1))
    isLNat#(n__tail(V1)) -> activate#(V1)
    isLNat#(n__tail(V1)) -> isLNatKind#(activate(V1))
    isLNat#(n__tail(V1)) -> U91#(isLNatKind(activate(V1)),activate(V1))
    isLNat#(n__take(V1,V2)) -> activate#(V2)
    isLNat#(n__take(V1,V2)) -> activate#(V1)
    isLNat#(n__take(V1,V2)) -> isNaturalKind#(activate(V1))
    isLNat#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNat#(n__take(V1,V2)) ->
    U101#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isLNatKind#(n__afterNth(V1,V2)) -> activate#(V2)
    isLNatKind#(n__afterNth(V1,V2)) -> activate#(V1)
    isLNatKind#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1))
    isLNatKind#(n__afterNth(V1,V2)) ->
    and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNatKind#(n__cons(V1,V2)) -> activate#(V2)
    isLNatKind#(n__cons(V1,V2)) -> activate#(V1)
    isLNatKind#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1))
    isLNatKind#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNatKind#(n__fst(V1)) -> activate#(V1)
    isLNatKind#(n__fst(V1)) -> isPLNatKind#(activate(V1))
    isLNatKind#(n__natsFrom(V1)) -> activate#(V1)
    isLNatKind#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1))
    isLNatKind#(n__snd(V1)) -> activate#(V1)
    isLNatKind#(n__snd(V1)) -> isPLNatKind#(activate(V1))
    isLNatKind#(n__tail(V1)) -> activate#(V1)
    isLNatKind#(n__tail(V1)) -> isLNatKind#(activate(V1))
    isLNatKind#(n__take(V1,V2)) -> activate#(V2)
    isLNatKind#(n__take(V1,V2)) -> activate#(V1)
    isLNatKind#(n__take(V1,V2)) -> isNaturalKind#(activate(V1))
    isLNatKind#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isNatural#(n__head(V1)) -> activate#(V1)
    isNatural#(n__head(V1)) -> isLNatKind#(activate(V1))
    isNatural#(n__head(V1)) -> U111#(isLNatKind(activate(V1)),activate(V1))
    isNatural#(n__s(V1)) -> activate#(V1)
    isNatural#(n__s(V1)) -> isNaturalKind#(activate(V1))
    isNatural#(n__s(V1)) -> U121#(isNaturalKind(activate(V1)),activate(V1))
    isNatural#(n__sel(V1,V2)) -> activate#(V2)
    isNatural#(n__sel(V1,V2)) -> activate#(V1)
    isNatural#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1))
    isNatural#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isNatural#(n__sel(V1,V2)) ->
    U131#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isNaturalKind#(n__head(V1)) -> activate#(V1)
    isNaturalKind#(n__head(V1)) -> isLNatKind#(activate(V1))
    isNaturalKind#(n__s(V1)) -> activate#(V1)
    isNaturalKind#(n__s(V1)) -> isNaturalKind#(activate(V1))
    isNaturalKind#(n__sel(V1,V2)) -> activate#(V2)
    isNaturalKind#(n__sel(V1,V2)) -> activate#(V1)
    isNaturalKind#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1))
    isNaturalKind#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isPLNat#(n__pair(V1,V2)) -> activate#(V2)
    isPLNat#(n__pair(V1,V2)) -> activate#(V1)
    isPLNat#(n__pair(V1,V2)) -> isLNatKind#(activate(V1))
    isPLNat#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
    isPLNat#(n__pair(V1,V2)) ->
    U141#(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isPLNat#(n__splitAt(V1,V2)) -> activate#(V2)
    isPLNat#(n__splitAt(V1,V2)) -> activate#(V1)
    isPLNat#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1))
    isPLNat#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isPLNat#(n__splitAt(V1,V2)) ->
    U151#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isPLNatKind#(n__pair(V1,V2)) -> activate#(V2)
    isPLNatKind#(n__pair(V1,V2)) -> activate#(V1)
    isPLNatKind#(n__pair(V1,V2)) -> isLNatKind#(activate(V1))
    isPLNatKind#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
    isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V2)
    isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V1)
    isPLNatKind#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1))
    isPLNatKind#(n__splitAt(V1,V2)) ->
    and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    natsFrom#(N) -> isNatural#(N)
    natsFrom#(N) -> and#(isNatural(N),n__isNaturalKind(N))
    natsFrom#(N) -> U161#(and(isNatural(N),n__isNaturalKind(N)),N)
    sel#(N,XS) -> isLNat#(XS)
    sel#(N,XS) -> isNatural#(N)
    sel#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
    sel#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
    sel#(N,XS) ->
    U171#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    snd#(pair(X,Y)) -> isLNat#(Y)
    snd#(pair(X,Y)) -> isLNat#(X)
    snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X))
    snd#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
    snd#(pair(X,Y)) ->
    U181#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
    splitAt#(0(),XS) -> isLNat#(XS)
    splitAt#(0(),XS) -> and#(isLNat(XS),n__isLNatKind(XS))
    splitAt#(0(),XS) -> U191#(and(isLNat(XS),n__isLNatKind(XS)),XS)
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    splitAt#(s(N),cons(X,XS)) -> isLNat#(activate(XS))
    splitAt#(s(N),cons(X,XS)) -> isNatural#(X)
    splitAt#(s(N),cons(X,XS)) -> and#(isNatural(X),n__isNaturalKind(X))
    splitAt#(s(N),cons(X,XS)) -> isNatural#(N)
    splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
    splitAt#(s(N),cons(X,XS)) ->
    and#(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                      n__and(isLNat(activate(XS)),
                                                             n__isLNatKind
                                                             (activate(XS)))))
    splitAt#(s(N),cons(X,XS)) ->
    U201#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                           n__and(isLNat(activate(XS)),
                                                                  n__isLNatKind
                                                                  (activate(XS))))),
          N,X,activate(XS))
    tail#(cons(N,XS)) -> activate#(XS)
    tail#(cons(N,XS)) -> isLNat#(activate(XS))
    tail#(cons(N,XS)) -> isNatural#(N)
    tail#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
    tail#(cons(N,XS)) ->
    and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                      n__isLNatKind(activate(XS))))
    tail#(cons(N,XS)) ->
    U211#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                           n__isLNatKind
                                                           (activate(XS)))),
          activate(XS))
    take#(N,XS) -> isLNat#(XS)
    take#(N,XS) -> isNatural#(N)
    take#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
    take#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
    take#(N,XS) ->
    U221#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    activate#(n__isNaturalKind(X)) -> isNaturalKind#(X)
    activate#(n__and(X1,X2)) -> and#(X1,X2)
    activate#(n__isLNatKind(X)) -> isLNatKind#(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)
   TRS:
    U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2))
    U102(tt(),V2) -> U103(isLNat(activate(V2)))
    U103(tt()) -> tt()
    U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    U111(tt(),V1) -> U112(isLNat(activate(V1)))
    U112(tt()) -> tt()
    U121(tt(),V1) -> U122(isNatural(activate(V1)))
    U122(tt()) -> tt()
    U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2))
    U132(tt(),V2) -> U133(isLNat(activate(V2)))
    U133(tt()) -> tt()
    U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2))
    U142(tt(),V2) -> U143(isLNat(activate(V2)))
    U143(tt()) -> tt()
    U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2))
    U152(tt(),V2) -> U153(isLNat(activate(V2)))
    U153(tt()) -> tt()
    U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N))))
    U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
    U181(tt(),Y) -> activate(Y)
    U191(tt(),XS) -> pair(nil(),activate(XS))
    U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X))
    U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    U21(tt(),X) -> activate(X)
    U211(tt(),XS) -> activate(XS)
    U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
    U31(tt(),N) -> activate(N)
    U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2))
    U42(tt(),V2) -> U43(isLNat(activate(V2)))
    U43(tt()) -> tt()
    U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2))
    U52(tt(),V2) -> U53(isLNat(activate(V2)))
    U53(tt()) -> tt()
    U61(tt(),V1) -> U62(isPLNat(activate(V1)))
    U62(tt()) -> tt()
    U71(tt(),V1) -> U72(isNatural(activate(V1)))
    U72(tt()) -> tt()
    U81(tt(),V1) -> U82(isPLNat(activate(V1)))
    U82(tt()) -> tt()
    U91(tt(),V1) -> U92(isLNat(activate(V1)))
    U92(tt()) -> tt()
    afterNth(N,XS) ->
    U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    and(tt(),X) -> activate(X)
    fst(pair(X,Y)) ->
    U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
    head(cons(N,XS)) ->
    U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                         n__isLNatKind
                                                         (activate(XS)))),
        N)
    isLNat(n__nil()) -> tt()
    isLNat(n__afterNth(V1,V2)) ->
    U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isLNat(n__cons(V1,V2)) ->
    U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1))
    isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1))
    isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1))
    isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1))
    isLNat(n__take(V1,V2)) ->
    U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isLNatKind(n__nil()) -> tt()
    isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
    isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
    isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
    isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
    isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isNatural(n__0()) -> tt()
    isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1))
    isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1))
    isNatural(n__sel(V1,V2)) ->
    U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isNaturalKind(n__0()) -> tt()
    isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
    isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
    isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    isPLNat(n__pair(V1,V2)) ->
    U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isPLNat(n__splitAt(V1,V2)) ->
    U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
    isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N)
    sel(N,XS) ->
    U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    snd(pair(X,Y)) ->
    U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
    splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS)
    splitAt(s(N),cons(X,XS)) ->
    U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                          n__and(isLNat(activate(XS)),
                                                                 n__isLNatKind
                                                                 (activate(XS))))),
         N,X,activate(XS))
    tail(cons(N,XS)) ->
    U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                          n__isLNatKind
                                                          (activate(XS)))),
         activate(XS))
    take(N,XS) ->
    U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    natsFrom(X) -> n__natsFrom(X)
    isNaturalKind(X) -> n__isNaturalKind(X)
    and(X1,X2) -> n__and(X1,X2)
    isLNatKind(X) -> n__isLNatKind(X)
    nil() -> n__nil()
    afterNth(X1,X2) -> n__afterNth(X1,X2)
    cons(X1,X2) -> n__cons(X1,X2)
    fst(X) -> n__fst(X)
    snd(X) -> n__snd(X)
    tail(X) -> n__tail(X)
    take(X1,X2) -> n__take(X1,X2)
    0() -> n__0()
    head(X) -> n__head(X)
    s(X) -> n__s(X)
    sel(X1,X2) -> n__sel(X1,X2)
    pair(X1,X2) -> n__pair(X1,X2)
    splitAt(X1,X2) -> n__splitAt(X1,X2)
    activate(n__natsFrom(X)) -> natsFrom(X)
    activate(n__isNaturalKind(X)) -> isNaturalKind(X)
    activate(n__and(X1,X2)) -> and(X1,X2)
    activate(n__isLNatKind(X)) -> isLNatKind(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)
    activate(X) -> X
   graph:
    ...
   SCC Processor:
    #sccs: 1
    #rules: 220
    #arcs: 2604/59049
    DPs:
     take#(N,XS) ->
     and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
     and#(tt(),X) -> activate#(X)
     activate#(n__natsFrom(X)) -> natsFrom#(X)
     natsFrom#(N) -> isNatural#(N)
     isNatural#(n__head(V1)) -> activate#(V1)
     activate#(n__isNaturalKind(X)) -> isNaturalKind#(X)
     isNaturalKind#(n__head(V1)) -> activate#(V1)
     activate#(n__and(X1,X2)) -> and#(X1,X2)
     activate#(n__isLNatKind(X)) -> isLNatKind#(X)
     isLNatKind#(n__afterNth(V1,V2)) -> activate#(V2)
     activate#(n__afterNth(X1,X2)) -> afterNth#(X1,X2)
     afterNth#(N,XS) -> isLNat#(XS)
     isLNat#(n__afterNth(V1,V2)) -> activate#(V2)
     activate#(n__fst(X)) -> fst#(X)
     fst#(pair(X,Y)) -> isLNat#(Y)
     isLNat#(n__afterNth(V1,V2)) -> activate#(V1)
     activate#(n__snd(X)) -> snd#(X)
     snd#(pair(X,Y)) -> isLNat#(Y)
     isLNat#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1))
     isNaturalKind#(n__head(V1)) -> isLNatKind#(activate(V1))
     isLNatKind#(n__afterNth(V1,V2)) -> activate#(V1)
     activate#(n__tail(X)) -> tail#(X)
     tail#(cons(N,XS)) -> activate#(XS)
     activate#(n__take(X1,X2)) -> take#(X1,X2)
     take#(N,XS) -> isLNat#(XS)
     isLNat#(n__afterNth(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNat#(n__afterNth(V1,V2)) ->
     U41#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     U41#(tt(),V1,V2) -> activate#(V2)
     activate#(n__head(X)) -> head#(X)
     head#(cons(N,XS)) -> activate#(XS)
     activate#(n__sel(X1,X2)) -> sel#(X1,X2)
     sel#(N,XS) -> isLNat#(XS)
     isLNat#(n__cons(V1,V2)) -> activate#(V2)
     activate#(n__splitAt(X1,X2)) -> splitAt#(X1,X2)
     splitAt#(0(),XS) -> isLNat#(XS)
     isLNat#(n__cons(V1,V2)) -> activate#(V1)
     isLNat#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1))
     isNaturalKind#(n__s(V1)) -> activate#(V1)
     isNaturalKind#(n__s(V1)) -> isNaturalKind#(activate(V1))
     isNaturalKind#(n__sel(V1,V2)) -> activate#(V2)
     isNaturalKind#(n__sel(V1,V2)) -> activate#(V1)
     isNaturalKind#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1))
     isNaturalKind#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNat#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNat#(n__cons(V1,V2)) ->
     U51#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     U51#(tt(),V1,V2) -> activate#(V2)
     U51#(tt(),V1,V2) -> activate#(V1)
     U51#(tt(),V1,V2) -> isNatural#(activate(V1))
     isNatural#(n__head(V1)) -> isLNatKind#(activate(V1))
     isLNatKind#(n__afterNth(V1,V2)) -> isNaturalKind#(activate(V1))
     isLNatKind#(n__afterNth(V1,V2)) ->
     and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNatKind#(n__cons(V1,V2)) -> activate#(V2)
     isLNatKind#(n__cons(V1,V2)) -> activate#(V1)
     isLNatKind#(n__cons(V1,V2)) -> isNaturalKind#(activate(V1))
     isLNatKind#(n__cons(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNatKind#(n__fst(V1)) -> activate#(V1)
     isLNatKind#(n__fst(V1)) -> isPLNatKind#(activate(V1))
     isPLNatKind#(n__pair(V1,V2)) -> activate#(V2)
     isPLNatKind#(n__pair(V1,V2)) -> activate#(V1)
     isPLNatKind#(n__pair(V1,V2)) -> isLNatKind#(activate(V1))
     isLNatKind#(n__natsFrom(V1)) -> activate#(V1)
     isLNatKind#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1))
     isLNatKind#(n__snd(V1)) -> activate#(V1)
     isLNatKind#(n__snd(V1)) -> isPLNatKind#(activate(V1))
     isPLNatKind#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
     isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V2)
     isPLNatKind#(n__splitAt(V1,V2)) -> activate#(V1)
     isPLNatKind#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1))
     isPLNatKind#(n__splitAt(V1,V2)) ->
     and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNatKind#(n__tail(V1)) -> activate#(V1)
     isLNatKind#(n__tail(V1)) -> isLNatKind#(activate(V1))
     isLNatKind#(n__take(V1,V2)) -> activate#(V2)
     isLNatKind#(n__take(V1,V2)) -> activate#(V1)
     isLNatKind#(n__take(V1,V2)) -> isNaturalKind#(activate(V1))
     isLNatKind#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isNatural#(n__head(V1)) -> U111#(isLNatKind(activate(V1)),activate(V1))
     U111#(tt(),V1) -> activate#(V1)
     U111#(tt(),V1) -> isLNat#(activate(V1))
     isLNat#(n__fst(V1)) -> activate#(V1)
     isLNat#(n__fst(V1)) -> isPLNatKind#(activate(V1))
     isLNat#(n__fst(V1)) -> U61#(isPLNatKind(activate(V1)),activate(V1))
     U61#(tt(),V1) -> activate#(V1)
     U61#(tt(),V1) -> isPLNat#(activate(V1))
     isPLNat#(n__pair(V1,V2)) -> activate#(V2)
     isPLNat#(n__pair(V1,V2)) -> activate#(V1)
     isPLNat#(n__pair(V1,V2)) -> isLNatKind#(activate(V1))
     isPLNat#(n__pair(V1,V2)) -> and#(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
     isPLNat#(n__pair(V1,V2)) ->
     U141#(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     U141#(tt(),V1,V2) -> activate#(V2)
     U141#(tt(),V1,V2) -> activate#(V1)
     U141#(tt(),V1,V2) -> isLNat#(activate(V1))
     isLNat#(n__natsFrom(V1)) -> activate#(V1)
     isLNat#(n__natsFrom(V1)) -> isNaturalKind#(activate(V1))
     isLNat#(n__natsFrom(V1)) -> U71#(isNaturalKind(activate(V1)),activate(V1))
     U71#(tt(),V1) -> activate#(V1)
     U71#(tt(),V1) -> isNatural#(activate(V1))
     isNatural#(n__s(V1)) -> activate#(V1)
     isNatural#(n__s(V1)) -> isNaturalKind#(activate(V1))
     isNatural#(n__s(V1)) -> U121#(isNaturalKind(activate(V1)),activate(V1))
     U121#(tt(),V1) -> activate#(V1)
     U121#(tt(),V1) -> isNatural#(activate(V1))
     isNatural#(n__sel(V1,V2)) -> activate#(V2)
     isNatural#(n__sel(V1,V2)) -> activate#(V1)
     isNatural#(n__sel(V1,V2)) -> isNaturalKind#(activate(V1))
     isNatural#(n__sel(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isNatural#(n__sel(V1,V2)) ->
     U131#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     U131#(tt(),V1,V2) -> activate#(V2)
     U131#(tt(),V1,V2) -> activate#(V1)
     U131#(tt(),V1,V2) -> isNatural#(activate(V1))
     U131#(tt(),V1,V2) -> U132#(isNatural(activate(V1)),activate(V2))
     U132#(tt(),V2) -> activate#(V2)
     U132#(tt(),V2) -> isLNat#(activate(V2))
     isLNat#(n__snd(V1)) -> activate#(V1)
     isLNat#(n__snd(V1)) -> isPLNatKind#(activate(V1))
     isLNat#(n__snd(V1)) -> U81#(isPLNatKind(activate(V1)),activate(V1))
     U81#(tt(),V1) -> activate#(V1)
     U81#(tt(),V1) -> isPLNat#(activate(V1))
     isPLNat#(n__splitAt(V1,V2)) -> activate#(V2)
     isPLNat#(n__splitAt(V1,V2)) -> activate#(V1)
     isPLNat#(n__splitAt(V1,V2)) -> isNaturalKind#(activate(V1))
     isPLNat#(n__splitAt(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isPLNat#(n__splitAt(V1,V2)) ->
     U151#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     U151#(tt(),V1,V2) -> activate#(V2)
     U151#(tt(),V1,V2) -> activate#(V1)
     U151#(tt(),V1,V2) -> isNatural#(activate(V1))
     U151#(tt(),V1,V2) -> U152#(isNatural(activate(V1)),activate(V2))
     U152#(tt(),V2) -> activate#(V2)
     U152#(tt(),V2) -> isLNat#(activate(V2))
     isLNat#(n__tail(V1)) -> activate#(V1)
     isLNat#(n__tail(V1)) -> isLNatKind#(activate(V1))
     isLNat#(n__tail(V1)) -> U91#(isLNatKind(activate(V1)),activate(V1))
     U91#(tt(),V1) -> activate#(V1)
     U91#(tt(),V1) -> isLNat#(activate(V1))
     isLNat#(n__take(V1,V2)) -> activate#(V2)
     isLNat#(n__take(V1,V2)) -> activate#(V1)
     isLNat#(n__take(V1,V2)) -> isNaturalKind#(activate(V1))
     isLNat#(n__take(V1,V2)) -> and#(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNat#(n__take(V1,V2)) ->
     U101#(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     U101#(tt(),V1,V2) -> activate#(V2)
     U101#(tt(),V1,V2) -> activate#(V1)
     U101#(tt(),V1,V2) -> isNatural#(activate(V1))
     U101#(tt(),V1,V2) -> U102#(isNatural(activate(V1)),activate(V2))
     U102#(tt(),V2) -> activate#(V2)
     U102#(tt(),V2) -> isLNat#(activate(V2))
     U141#(tt(),V1,V2) -> U142#(isLNat(activate(V1)),activate(V2))
     U142#(tt(),V2) -> activate#(V2)
     U142#(tt(),V2) -> isLNat#(activate(V2))
     U51#(tt(),V1,V2) -> U52#(isNatural(activate(V1)),activate(V2))
     U52#(tt(),V2) -> activate#(V2)
     U52#(tt(),V2) -> isLNat#(activate(V2))
     splitAt#(0(),XS) -> and#(isLNat(XS),n__isLNatKind(XS))
     splitAt#(0(),XS) -> U191#(and(isLNat(XS),n__isLNatKind(XS)),XS)
     U191#(tt(),XS) -> activate#(XS)
     splitAt#(s(N),cons(X,XS)) -> activate#(XS)
     splitAt#(s(N),cons(X,XS)) -> isLNat#(activate(XS))
     splitAt#(s(N),cons(X,XS)) -> isNatural#(X)
     splitAt#(s(N),cons(X,XS)) -> and#(isNatural(X),n__isNaturalKind(X))
     splitAt#(s(N),cons(X,XS)) -> isNatural#(N)
     splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
     splitAt#(s(N),cons(X,XS)) ->
     and#(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                       n__and(isLNat(activate(XS)),
                                                              n__isLNatKind
                                                              (activate(XS)))))
     splitAt#(s(N),cons(X,XS)) ->
     U201#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                            n__and(isLNat(activate(XS)),
                                                                   n__isLNatKind
                                                                   (activate(XS))))),
           N,X,activate(XS))
     U201#(tt(),N,X,XS) -> activate#(X)
     U201#(tt(),N,X,XS) -> activate#(XS)
     U201#(tt(),N,X,XS) -> activate#(N)
     U201#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
     U201#(tt(),N,X,XS) -> U202#(splitAt(activate(N),activate(XS)),activate(X))
     U202#(pair(YS,ZS),X) -> activate#(X)
     sel#(N,XS) -> isNatural#(N)
     sel#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
     sel#(N,XS) -> and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
     sel#(N,XS) ->
     U171#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
     U171#(tt(),N,XS) -> activate#(XS)
     U171#(tt(),N,XS) -> activate#(N)
     U171#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
     afterNth#(N,XS) -> isNatural#(N)
     afterNth#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
     afterNth#(N,XS) ->
     and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
     afterNth#(N,XS) ->
     U11#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
     U11#(tt(),N,XS) -> activate#(XS)
     U11#(tt(),N,XS) -> activate#(N)
     U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
     U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
     snd#(pair(X,Y)) -> isLNat#(X)
     snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X))
     snd#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
     snd#(pair(X,Y)) ->
     U181#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
     U181#(tt(),Y) -> activate#(Y)
     U171#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
     head#(cons(N,XS)) -> isLNat#(activate(XS))
     head#(cons(N,XS)) -> isNatural#(N)
     head#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
     head#(cons(N,XS)) ->
     and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                       n__isLNatKind(activate(XS))))
     head#(cons(N,XS)) ->
     U31#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                           n__isLNatKind
                                                           (activate(XS)))),
          N)
     U31#(tt(),N) -> activate#(N)
     U41#(tt(),V1,V2) -> activate#(V1)
     U41#(tt(),V1,V2) -> isNatural#(activate(V1))
     U41#(tt(),V1,V2) -> U42#(isNatural(activate(V1)),activate(V2))
     U42#(tt(),V2) -> activate#(V2)
     U42#(tt(),V2) -> isLNat#(activate(V2))
     take#(N,XS) -> isNatural#(N)
     take#(N,XS) -> and#(isNatural(N),n__isNaturalKind(N))
     take#(N,XS) ->
     U221#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
     U221#(tt(),N,XS) -> activate#(XS)
     U221#(tt(),N,XS) -> activate#(N)
     U221#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
     U221#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
     fst#(pair(X,Y)) -> isLNat#(X)
     fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNatKind(X))
     fst#(pair(X,Y)) -> and#(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
     fst#(pair(X,Y)) ->
     U21#(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
     U21#(tt(),X) -> activate#(X)
     tail#(cons(N,XS)) -> isLNat#(activate(XS))
     tail#(cons(N,XS)) -> isNatural#(N)
     tail#(cons(N,XS)) -> and#(isNatural(N),n__isNaturalKind(N))
     tail#(cons(N,XS)) ->
     and#(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                       n__isLNatKind(activate(XS))))
     tail#(cons(N,XS)) ->
     U211#(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                            n__isLNatKind
                                                            (activate(XS)))),
           activate(XS))
     U211#(tt(),XS) -> activate#(XS)
     natsFrom#(N) -> and#(isNatural(N),n__isNaturalKind(N))
     natsFrom#(N) -> U161#(and(isNatural(N),n__isNaturalKind(N)),N)
     U161#(tt(),N) -> activate#(N)
    TRS:
     U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2))
     U102(tt(),V2) -> U103(isLNat(activate(V2)))
     U103(tt()) -> tt()
     U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
     U111(tt(),V1) -> U112(isLNat(activate(V1)))
     U112(tt()) -> tt()
     U121(tt(),V1) -> U122(isNatural(activate(V1)))
     U122(tt()) -> tt()
     U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2))
     U132(tt(),V2) -> U133(isLNat(activate(V2)))
     U133(tt()) -> tt()
     U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2))
     U142(tt(),V2) -> U143(isLNat(activate(V2)))
     U143(tt()) -> tt()
     U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2))
     U152(tt(),V2) -> U153(isLNat(activate(V2)))
     U153(tt()) -> tt()
     U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N))))
     U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
     U181(tt(),Y) -> activate(Y)
     U191(tt(),XS) -> pair(nil(),activate(XS))
     U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X))
     U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
     U21(tt(),X) -> activate(X)
     U211(tt(),XS) -> activate(XS)
     U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
     U31(tt(),N) -> activate(N)
     U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2))
     U42(tt(),V2) -> U43(isLNat(activate(V2)))
     U43(tt()) -> tt()
     U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2))
     U52(tt(),V2) -> U53(isLNat(activate(V2)))
     U53(tt()) -> tt()
     U61(tt(),V1) -> U62(isPLNat(activate(V1)))
     U62(tt()) -> tt()
     U71(tt(),V1) -> U72(isNatural(activate(V1)))
     U72(tt()) -> tt()
     U81(tt(),V1) -> U82(isPLNat(activate(V1)))
     U82(tt()) -> tt()
     U91(tt(),V1) -> U92(isLNat(activate(V1)))
     U92(tt()) -> tt()
     afterNth(N,XS) ->
     U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
     and(tt(),X) -> activate(X)
     fst(pair(X,Y)) ->
     U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
     head(cons(N,XS)) ->
     U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                          n__isLNatKind
                                                          (activate(XS)))),
         N)
     isLNat(n__nil()) -> tt()
     isLNat(n__afterNth(V1,V2)) ->
     U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     isLNat(n__cons(V1,V2)) ->
     U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1))
     isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1))
     isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1))
     isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1))
     isLNat(n__take(V1,V2)) ->
     U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     isLNatKind(n__nil()) -> tt()
     isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
     isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
     isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
     isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
     isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isNatural(n__0()) -> tt()
     isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1))
     isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1))
     isNatural(n__sel(V1,V2)) ->
     U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     isNaturalKind(n__0()) -> tt()
     isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
     isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
     isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     isPLNat(n__pair(V1,V2)) ->
     U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     isPLNat(n__splitAt(V1,V2)) ->
     U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
     isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
     isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
     natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N)
     sel(N,XS) ->
     U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
     snd(pair(X,Y)) ->
     U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
     splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS)
     splitAt(s(N),cons(X,XS)) ->
     U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),
                                                           n__and(isLNat(activate(XS)),
                                                                  n__isLNatKind
                                                                  (activate(XS))))),
          N,X,activate(XS))
     tail(cons(N,XS)) ->
     U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),
                                                           n__isLNatKind
                                                           (activate(XS)))),
          activate(XS))
     take(N,XS) ->
     U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
     natsFrom(X) -> n__natsFrom(X)
     isNaturalKind(X) -> n__isNaturalKind(X)
     and(X1,X2) -> n__and(X1,X2)
     isLNatKind(X) -> n__isLNatKind(X)
     nil() -> n__nil()
     afterNth(X1,X2) -> n__afterNth(X1,X2)
     cons(X1,X2) -> n__cons(X1,X2)
     fst(X) -> n__fst(X)
     snd(X) -> n__snd(X)
     tail(X) -> n__tail(X)
     take(X1,X2) -> n__take(X1,X2)
     0() -> n__0()
     head(X) -> n__head(X)
     s(X) -> n__s(X)
     sel(X1,X2) -> n__sel(X1,X2)
     pair(X1,X2) -> n__pair(X1,X2)
     splitAt(X1,X2) -> n__splitAt(X1,X2)
     activate(n__natsFrom(X)) -> natsFrom(X)
     activate(n__isNaturalKind(X)) -> isNaturalKind(X)
     activate(n__and(X1,X2)) -> and(X1,X2)
     activate(n__isLNatKind(X)) -> isLNatKind(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)
     activate(X) -> X
    Open