(STRATEGY
    INNERMOST)

(VAR
    N X XS Y YS ZS)
(DATATYPES
    A = µX.< tt, pair(X, X), cons(X, X), n__natsFrom(X), s(X), 0, nil >)
(SIGNATURES
    U11 :: [A x A x A] -> A
    U12 :: [A x A x A] -> A
    U21 :: [A x A] -> A
    U22 :: [A x A] -> A
    U31 :: [A x A] -> A
    U32 :: [A x A] -> A
    U41 :: [A x A x A] -> A
    U42 :: [A x A x A] -> A
    U51 :: [A x A] -> A
    U52 :: [A x A] -> A
    U61 :: [A x A x A x A] -> A
    U62 :: [A x A x A x A] -> A
    U63 :: [A x A x A x A] -> A
    U64 :: [A x A] -> A
    U71 :: [A x A] -> A
    U72 :: [A x A] -> A
    U81 :: [A x A x A] -> A
    U82 :: [A x A x A] -> A
    afterNth :: [A x A] -> A
    fst :: [A] -> A
    head :: [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
    activate :: [A] -> A)
(RULES
    U11(tt(),N,XS) -> U12(tt()
                         ,activate(N)
                         ,activate(XS))
    U12(tt(),N,XS) ->
      snd(splitAt(activate(N)
                 ,activate(XS)))
    U21(tt(),X) -> U22(tt()
                      ,activate(X))
    U22(tt(),X) -> activate(X)
    U31(tt(),N) -> U32(tt()
                      ,activate(N))
    U32(tt(),N) -> activate(N)
    U41(tt(),N,XS) -> U42(tt()
                         ,activate(N)
                         ,activate(XS))
    U42(tt(),N,XS) ->
      head(afterNth(activate(N)
                   ,activate(XS)))
    U51(tt(),Y) -> U52(tt()
                      ,activate(Y))
    U52(tt(),Y) -> activate(Y)
    U61(tt(),N,X,XS) -> U62(tt()
                           ,activate(N)
                           ,activate(X)
                           ,activate(XS))
    U62(tt(),N,X,XS) -> U63(tt()
                           ,activate(N)
                           ,activate(X)
                           ,activate(XS))
    U63(tt(),N,X,XS) ->
      U64(splitAt(activate(N)
                 ,activate(XS))
         ,activate(X))
    U64(pair(YS,ZS),X) ->
      pair(cons(activate(X),YS),ZS)
    U71(tt(),XS) -> U72(tt()
                       ,activate(XS))
    U72(tt(),XS) -> activate(XS)
    U81(tt(),N,XS) -> U82(tt()
                         ,activate(N)
                         ,activate(XS))
    U82(tt(),N,XS) ->
      fst(splitAt(activate(N)
                 ,activate(XS)))
    afterNth(N,XS) -> U11(tt(),N,XS)
    fst(pair(X,Y)) -> U21(tt(),X)
    head(cons(N,XS)) -> U31(tt(),N)
    natsFrom(N) -> cons(N
                       ,n__natsFrom(s(N)))
    sel(N,XS) -> U41(tt(),N,XS)
    snd(pair(X,Y)) -> U51(tt(),Y)
    splitAt(0(),XS) -> pair(nil()
                           ,XS)
    splitAt(s(N),cons(X,XS)) ->
      U61(tt(),N,X,activate(XS))
    tail(cons(N,XS)) -> U71(tt()
                           ,activate(XS))
    take(N,XS) -> U81(tt(),N,XS)
    natsFrom(X) -> n__natsFrom(X)
    activate(n__natsFrom(X)) ->
      natsFrom(X)
    activate(X) -> X)