(STRATEGY
    INNERMOST)

(VAR
    N V1 V2 X X1 X2 XS Y YS ZS)
(DATATYPES
    A = µX.< tt, n__natsFrom(X), n__s(X), n__isLNat(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__sel(X, X), n__pair(X, X), n__splitAt(X, X), n__and(X, X), n__isNatural(X) >)
(SIGNATURES
    U101 :: [A x A x A] -> A
    U11 :: [A x A x A] -> A
    U21 :: [A x A] -> A
    U31 :: [A x A] -> A
    U41 :: [A x A] -> A
    U51 :: [A x A x A] -> A
    U61 :: [A x A] -> A
    U71 :: [A x A] -> A
    U81 :: [A x A x A x A] -> A
    U82 :: [A x A] -> A
    U91 :: [A x A] -> A
    afterNth :: [A x A] -> A
    and :: [A x A] -> A
    fst :: [A] -> A
    head :: [A] -> A
    isLNat :: [A] -> A
    isNatural :: [A] -> A
    isPLNat :: [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
    s :: [A] -> A
    nil :: [] -> A
    cons :: [A x A] -> A
    0 :: [] -> A
    pair :: [A x A] -> A
    activate :: [A] -> A)
(RULES
    U101(tt(),N,XS) ->
      fst(splitAt(activate(N)
                 ,activate(XS)))
    U11(tt(),N,XS) ->
      snd(splitAt(activate(N)
                 ,activate(XS)))
    U21(tt(),X) -> activate(X)
    U31(tt(),N) -> activate(N)
    U41(tt(),N) -> cons(activate(N)
                       ,n__natsFrom(n__s(activate(N))))
    U51(tt(),N,XS) ->
      head(afterNth(activate(N)
                   ,activate(XS)))
    U61(tt(),Y) -> activate(Y)
    U71(tt(),XS) -> pair(nil()
                        ,activate(XS))
    U81(tt(),N,X,XS) ->
      U82(splitAt(activate(N)
                 ,activate(XS))
         ,activate(X))
    U82(pair(YS,ZS),X) ->
      pair(cons(activate(X),YS),ZS)
    U91(tt(),XS) -> activate(XS)
    afterNth(N,XS) ->
      U11(and(isNatural(N)
             ,n__isLNat(XS))
         ,N
         ,XS)
    and(tt(),X) -> activate(X)
    fst(pair(X,Y)) ->
      U21(and(isLNat(X),n__isLNat(Y))
         ,X)
    head(cons(N,XS)) ->
      U31(and(isNatural(N)
             ,n__isLNat(activate(XS)))
         ,N)
    isLNat(n__nil()) -> tt()
    isLNat(n__afterNth(V1,V2)) ->
      and(isNatural(activate(V1))
         ,n__isLNat(activate(V2)))
    isLNat(n__cons(V1,V2)) ->
      and(isNatural(activate(V1))
         ,n__isLNat(activate(V2)))
    isLNat(n__fst(V1)) ->
      isPLNat(activate(V1))
    isLNat(n__natsFrom(V1)) ->
      isNatural(activate(V1))
    isLNat(n__snd(V1)) ->
      isPLNat(activate(V1))
    isLNat(n__tail(V1)) ->
      isLNat(activate(V1))
    isLNat(n__take(V1,V2)) ->
      and(isNatural(activate(V1))
         ,n__isLNat(activate(V2)))
    isNatural(n__0()) -> tt()
    isNatural(n__head(V1)) ->
      isLNat(activate(V1))
    isNatural(n__s(V1)) ->
      isNatural(activate(V1))
    isNatural(n__sel(V1,V2)) ->
      and(isNatural(activate(V1))
         ,n__isLNat(activate(V2)))
    isPLNat(n__pair(V1,V2)) ->
      and(isLNat(activate(V1))
         ,n__isLNat(activate(V2)))
    isPLNat(n__splitAt(V1,V2)) ->
      and(isNatural(activate(V1))
         ,n__isLNat(activate(V2)))
    natsFrom(N) -> U41(isNatural(N)
                      ,N)
    sel(N,XS) ->
      U51(and(isNatural(N)
             ,n__isLNat(XS))
         ,N
         ,XS)
    snd(pair(X,Y)) ->
      U61(and(isLNat(X),n__isLNat(Y))
         ,Y)
    splitAt(0(),XS) ->
      U71(isLNat(XS),XS)
    splitAt(s(N),cons(X,XS)) ->
      U81(and(isNatural(N)
             ,n__and(n__isNatural(X)
                    ,n__isLNat(activate(XS))))
         ,N
         ,X
         ,activate(XS))
    tail(cons(N,XS)) ->
      U91(and(isNatural(N)
             ,n__isLNat(activate(XS)))
         ,activate(XS))
    take(N,XS) ->
      U101(and(isNatural(N)
              ,n__isLNat(XS))
          ,N
          ,XS)
    natsFrom(X) -> n__natsFrom(X)
    s(X) -> n__s(X)
    isLNat(X) -> n__isLNat(X)
    nil() -> n__nil()
    afterNth(X1,X2) ->
      n__afterNth(X1,X2)
    cons(X1,X2) -> n__cons(X1,X2)
    fst(X) -> n__fst(X)
    snd(X) -> n__snd(X)
    tail(X) -> n__tail(X)
    take(X1,X2) -> n__take(X1,X2)
    0() -> n__0()
    head(X) -> n__head(X)
    sel(X1,X2) -> n__sel(X1,X2)
    pair(X1,X2) -> n__pair(X1,X2)
    splitAt(X1,X2) -> n__splitAt(X1
                                ,X2)
    and(X1,X2) -> n__and(X1,X2)
    isNatural(X) -> n__isNatural(X)
    activate(n__natsFrom(X)) ->
      natsFrom(activate(X))
    activate(n__s(X)) ->
      s(activate(X))
    activate(n__isLNat(X)) ->
      isLNat(X)
    activate(n__nil()) -> nil()
    activate(n__afterNth(X1,X2)) ->
      afterNth(activate(X1)
              ,activate(X2))
    activate(n__cons(X1,X2)) ->
      cons(activate(X1),X2)
    activate(n__fst(X)) ->
      fst(activate(X))
    activate(n__snd(X)) ->
      snd(activate(X))
    activate(n__tail(X)) ->
      tail(activate(X))
    activate(n__take(X1,X2)) ->
      take(activate(X1),activate(X2))
    activate(n__0()) -> 0()
    activate(n__head(X)) ->
      head(activate(X))
    activate(n__sel(X1,X2)) ->
      sel(activate(X1),activate(X2))
    activate(n__pair(X1,X2)) ->
      pair(activate(X1),activate(X2))
    activate(n__splitAt(X1,X2)) ->
      splitAt(activate(X1)
             ,activate(X2))
    activate(n__and(X1,X2)) ->
      and(activate(X1),X2)
    activate(n__isNatural(X)) ->
      isNatural(X)
    activate(X) -> X)