(STRATEGY
    INNERMOST)

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