YES
Time: 0.028393
TRS:
 {               natsFrom N -> cons(N, n__natsFrom n__s N),
                 natsFrom X -> n__natsFrom X,
           fst pair(XS, YS) -> XS,
           snd pair(XS, YS) -> YS,
           splitAt(0(), XS) -> pair(nil(), XS),
  splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
  u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                 activate X -> X,
     activate n__natsFrom X -> natsFrom activate X,
            activate n__s X -> s activate X,
                        s X -> n__s X,
           head cons(N, XS) -> N,
           tail cons(N, XS) -> activate XS,
            afterNth(N, XS) -> snd splitAt(N, XS),
                 sel(N, XS) -> head afterNth(N, XS),
                take(N, XS) -> fst splitAt(N, XS)}
 DP:
  DP:
   {splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS),
    splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS),
    splitAt#(s N, cons(X, XS)) -> activate# XS,
    u#(pair(YS, ZS), N, X, XS) -> activate# X,
       activate# n__natsFrom X -> natsFrom# activate X,
       activate# n__natsFrom X -> activate# X,
              activate# n__s X -> activate# X,
              activate# n__s X -> s# activate X,
             tail# cons(N, XS) -> activate# XS,
              afterNth#(N, XS) -> snd# splitAt(N, XS),
              afterNth#(N, XS) -> splitAt#(N, XS),
                   sel#(N, XS) -> head# afterNth(N, XS),
                   sel#(N, XS) -> afterNth#(N, XS),
                  take#(N, XS) -> fst# splitAt(N, XS),
                  take#(N, XS) -> splitAt#(N, XS)}
  TRS:
  {               natsFrom N -> cons(N, n__natsFrom n__s N),
                  natsFrom X -> n__natsFrom X,
            fst pair(XS, YS) -> XS,
            snd pair(XS, YS) -> YS,
            splitAt(0(), XS) -> pair(nil(), XS),
   splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
   u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                  activate X -> X,
      activate n__natsFrom X -> natsFrom activate X,
             activate n__s X -> s activate X,
                         s X -> n__s X,
            head cons(N, XS) -> N,
            tail cons(N, XS) -> activate XS,
             afterNth(N, XS) -> snd splitAt(N, XS),
                  sel(N, XS) -> head afterNth(N, XS),
                 take(N, XS) -> fst splitAt(N, XS)}
  UR:
   {               natsFrom N -> cons(N, n__natsFrom n__s N),
                   natsFrom X -> n__natsFrom X,
             snd pair(XS, YS) -> YS,
             splitAt(0(), XS) -> pair(nil(), XS),
    splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
    u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                   activate X -> X,
       activate n__natsFrom X -> natsFrom activate X,
              activate n__s X -> s activate X,
                          s X -> n__s X,
              afterNth(N, XS) -> snd splitAt(N, XS),
                      a(x, y) -> x,
                      a(x, y) -> y}
   EDG:
    {(tail# cons(N, XS) -> activate# XS, activate# n__s X -> s# activate X)
     (tail# cons(N, XS) -> activate# XS, activate# n__s X -> activate# X)
     (tail# cons(N, XS) -> activate# XS, activate# n__natsFrom X -> activate# X)
     (tail# cons(N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# activate X)
     (afterNth#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> activate# XS)
     (afterNth#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS))
     (afterNth#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS))
     (take#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> activate# XS)
     (take#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS))
     (take#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS))
     (activate# n__natsFrom X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__natsFrom X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__natsFrom X -> activate# X, activate# n__natsFrom X -> activate# X)
     (activate# n__natsFrom X -> activate# X, activate# n__natsFrom X -> natsFrom# activate X)
     (splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS), u#(pair(YS, ZS), N, X, XS) -> activate# X)
     (activate# n__s X -> activate# X, activate# n__natsFrom X -> natsFrom# activate X)
     (activate# n__s X -> activate# X, activate# n__natsFrom X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (u#(pair(YS, ZS), N, X, XS) -> activate# X, activate# n__natsFrom X -> natsFrom# activate X)
     (u#(pair(YS, ZS), N, X, XS) -> activate# X, activate# n__natsFrom X -> activate# X)
     (u#(pair(YS, ZS), N, X, XS) -> activate# X, activate# n__s X -> activate# X)
     (u#(pair(YS, ZS), N, X, XS) -> activate# X, activate# n__s X -> s# activate X)
     (sel#(N, XS) -> afterNth#(N, XS), afterNth#(N, XS) -> snd# splitAt(N, XS))
     (sel#(N, XS) -> afterNth#(N, XS), afterNth#(N, XS) -> splitAt#(N, XS))
     (splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS), splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS))
     (splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS), splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS))
     (splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS), splitAt#(s N, cons(X, XS)) -> activate# XS)
     (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__natsFrom X -> natsFrom# activate X)
     (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__natsFrom X -> activate# X)
     (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> activate# X)
     (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> s# activate X)}
    STATUS:
     arrows: 0.857778
     SCCS (2):
      Scc:
       {splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS)}
      Scc:
       {activate# n__natsFrom X -> activate# X,
               activate# n__s X -> activate# X}
      
      
      
      
      
      
      
      SCC (1):
       Strict:
        {splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS)}
       Weak:
       {               natsFrom N -> cons(N, n__natsFrom n__s N),
                       natsFrom X -> n__natsFrom X,
                 fst pair(XS, YS) -> XS,
                 snd pair(XS, YS) -> YS,
                 splitAt(0(), XS) -> pair(nil(), XS),
        splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
        u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                       activate X -> X,
           activate n__natsFrom X -> natsFrom activate X,
                  activate n__s X -> s activate X,
                              s X -> n__s X,
                 head cons(N, XS) -> N,
                 tail cons(N, XS) -> activate XS,
                  afterNth(N, XS) -> snd splitAt(N, XS),
                       sel(N, XS) -> head afterNth(N, XS),
                      take(N, XS) -> fst splitAt(N, XS)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [u](x0, x1, x2, x3) = x0 + 1,
         
         [cons](x0, x1) = 0,
         
         [pair](x0, x1) = x0 + 1,
         
         [splitAt](x0, x1) = x0,
         
         [afterNth](x0, x1) = 0,
         
         [sel](x0, x1) = 0,
         
         [take](x0, x1) = 0,
         
         [n__natsFrom](x0) = 1,
         
         [n__s](x0) = 1,
         
         [natsFrom](x0) = x0 + 1,
         
         [fst](x0) = 0,
         
         [snd](x0) = x0 + 1,
         
         [activate](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [head](x0) = 0,
         
         [tail](x0) = 0,
         
         [nil] = 1,
         
         [0] = 0,
         
         [splitAt#](x0, x1) = x0
        Strict:
         splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS)
         1 + 1N + 0XS + 0X >= 0 + 1N + 0XS
        Weak:
         take(N, XS) -> fst splitAt(N, XS)
         0 + 0N + 0XS >= 0 + 0N + 0XS
         sel(N, XS) -> head afterNth(N, XS)
         0 + 0N + 0XS >= 0 + 0N + 0XS
         afterNth(N, XS) -> snd splitAt(N, XS)
         0 + 0N + 0XS >= 1 + 0N + 1XS
         tail cons(N, XS) -> activate XS
         0 + 0N + 0XS >= 1 + 1XS
         head cons(N, XS) -> N
         0 + 0N + 0XS >= 1N
         s X -> n__s X
         1 + 1X >= 1 + 0X
         activate n__s X -> s activate X
         2 + 0X >= 2 + 1X
         activate n__natsFrom X -> natsFrom activate X
         2 + 0X >= 2 + 1X
         activate X -> X
         1 + 1X >= 1X
         u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS)
         2 + 0N + 0XS + 1YS + 0X + 0ZS >= 1 + 0YS + 0X + 0ZS
         splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS)
         0 + 0N + 0XS + 0X >= 2 + 0N + 1XS + 0X
         splitAt(0(), XS) -> pair(nil(), XS)
         0 + 1XS >= 2 + 0XS
         snd pair(XS, YS) -> YS
         2 + 1XS + 0YS >= 1YS
         fst pair(XS, YS) -> XS
         0 + 0XS + 0YS >= 1XS
         natsFrom X -> n__natsFrom X
         1 + 1X >= 1 + 0X
         natsFrom N -> cons(N, n__natsFrom n__s N)
         1 + 1N >= 0 + 0N
       Qed
     
     
     
     
     SCC (2):
      Strict:
       {activate# n__natsFrom X -> activate# X,
               activate# n__s X -> activate# X}
      Weak:
      {               natsFrom N -> cons(N, n__natsFrom n__s N),
                      natsFrom X -> n__natsFrom X,
                fst pair(XS, YS) -> XS,
                snd pair(XS, YS) -> YS,
                splitAt(0(), XS) -> pair(nil(), XS),
       splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
       u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                      activate X -> X,
          activate n__natsFrom X -> natsFrom activate X,
                 activate n__s X -> s activate X,
                             s X -> n__s X,
                head cons(N, XS) -> N,
                tail cons(N, XS) -> activate XS,
                 afterNth(N, XS) -> snd splitAt(N, XS),
                      sel(N, XS) -> head afterNth(N, XS),
                     take(N, XS) -> fst splitAt(N, XS)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [u](x0, x1, x2, x3) = x0 + x1 + 1,
        
        [cons](x0, x1) = 0,
        
        [pair](x0, x1) = x0 + 1,
        
        [splitAt](x0, x1) = x0 + x1,
        
        [afterNth](x0, x1) = 0,
        
        [sel](x0, x1) = 0,
        
        [take](x0, x1) = 0,
        
        [n__natsFrom](x0) = x0 + 1,
        
        [n__s](x0) = x0 + 1,
        
        [natsFrom](x0) = x0 + 1,
        
        [fst](x0) = 0,
        
        [snd](x0) = x0 + 1,
        
        [activate](x0) = 1,
        
        [s](x0) = 0,
        
        [head](x0) = 0,
        
        [tail](x0) = 0,
        
        [nil] = 1,
        
        [0] = 0,
        
        [activate#](x0) = x0 + 1
       Strict:
        activate# n__s X -> activate# X
        2 + 1X >= 1 + 1X
        activate# n__natsFrom X -> activate# X
        2 + 1X >= 1 + 1X
       Weak:
        take(N, XS) -> fst splitAt(N, XS)
        0 + 0N + 0XS >= 0 + 0N + 0XS
        sel(N, XS) -> head afterNth(N, XS)
        0 + 0N + 0XS >= 0 + 0N + 0XS
        afterNth(N, XS) -> snd splitAt(N, XS)
        0 + 0N + 0XS >= 1 + 1N + 1XS
        tail cons(N, XS) -> activate XS
        0 + 0N + 0XS >= 1 + 0XS
        head cons(N, XS) -> N
        0 + 0N + 0XS >= 1N
        s X -> n__s X
        0 + 0X >= 1 + 1X
        activate n__s X -> s activate X
        1 + 0X >= 0 + 0X
        activate n__natsFrom X -> natsFrom activate X
        1 + 0X >= 2 + 0X
        activate X -> X
        1 + 0X >= 1X
        u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS)
        2 + 1N + 0XS + 1YS + 0X + 0ZS >= 1 + 0YS + 0X + 0ZS
        splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS)
        0 + 0N + 0XS + 0X >= 2 + 2N + 0XS + 0X
        splitAt(0(), XS) -> pair(nil(), XS)
        0 + 1XS >= 2 + 0XS
        snd pair(XS, YS) -> YS
        2 + 1XS + 0YS >= 1YS
        fst pair(XS, YS) -> XS
        0 + 0XS + 0YS >= 1XS
        natsFrom X -> n__natsFrom X
        1 + 1X >= 1 + 1X
        natsFrom N -> cons(N, n__natsFrom n__s N)
        1 + 1N >= 0 + 0N
      Qed