MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { natsFrom(N) -> cons(N, natsFrom(s(N)))
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
  , head(cons(N, XS)) -> N
  , tail(cons(N, XS)) -> XS
  , sel(N, XS) -> head(afterNth(N, XS))
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following weak dependency pairs:

Strict DPs:
  { natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
  , fst^#(pair(XS, YS)) -> c_2()
  , snd^#(pair(XS, YS)) -> c_3()
  , splitAt^#(s(N), cons(X, XS)) ->
    c_4(u^#(splitAt(N, XS), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , u^#(pair(YS, ZS), N, X, XS) -> c_6()
  , head^#(cons(N, XS)) -> c_7()
  , tail^#(cons(N, XS)) -> c_8()
  , sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
  , afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
  , take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
  , fst^#(pair(XS, YS)) -> c_2()
  , snd^#(pair(XS, YS)) -> c_3()
  , splitAt^#(s(N), cons(X, XS)) ->
    c_4(u^#(splitAt(N, XS), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , u^#(pair(YS, ZS), N, X, XS) -> c_6()
  , head^#(cons(N, XS)) -> c_7()
  , tail^#(cons(N, XS)) -> c_8()
  , sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
  , afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
  , take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Strict Trs:
  { natsFrom(N) -> cons(N, natsFrom(s(N)))
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
  , head(cons(N, XS)) -> N
  , tail(cons(N, XS)) -> XS
  , sel(N, XS) -> head(afterNth(N, XS))
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { snd(pair(XS, YS)) -> YS
    , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
    , splitAt(0(), XS) -> pair(nil(), XS)
    , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
    , afterNth(N, XS) -> snd(splitAt(N, XS)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
  , fst^#(pair(XS, YS)) -> c_2()
  , snd^#(pair(XS, YS)) -> c_3()
  , splitAt^#(s(N), cons(X, XS)) ->
    c_4(u^#(splitAt(N, XS), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , u^#(pair(YS, ZS), N, X, XS) -> c_6()
  , head^#(cons(N, XS)) -> c_7()
  , tail^#(cons(N, XS)) -> c_8()
  , sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
  , afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
  , take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Strict Trs:
  { snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
  , afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(snd) = {1}, Uargs(u) = {1}, Uargs(c_1) = {1},
  Uargs(fst^#) = {1}, Uargs(snd^#) = {1}, Uargs(c_4) = {1},
  Uargs(u^#) = {1}, Uargs(head^#) = {1}, Uargs(c_9) = {1},
  Uargs(c_10) = {1}, Uargs(c_11) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

         [cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                               
                [s](x1) = [1] x1 + [2]         
                                               
         [pair](x1, x2) = [1] x2 + [2]         
                                               
              [snd](x1) = [1] x1 + [1]         
                                               
      [splitAt](x1, x2) = [2] x1 + [2] x2 + [0]
                                               
                    [0] = [2]                  
                                               
                  [nil] = [2]                  
                                               
    [u](x1, x2, x3, x4) = [1] x1 + [1] x3 + [2]
                                               
     [afterNth](x1, x2) = [2] x1 + [2] x2 + [2]
                                               
       [natsFrom^#](x1) = [1] x1 + [1]         
                                               
              [c_1](x1) = [1] x1 + [1]         
                                               
            [fst^#](x1) = [1] x1 + [2]         
                                               
                  [c_2] = [1]                  
                                               
            [snd^#](x1) = [1] x1 + [2]         
                                               
                  [c_3] = [1]                  
                                               
    [splitAt^#](x1, x2) = [2] x1 + [2] x2 + [2]
                                               
              [c_4](x1) = [1] x1 + [2]         
                                               
  [u^#](x1, x2, x3, x4) = [1] x1 + [2] x3 + [2]
                                               
                  [c_5] = [1]                  
                                               
                  [c_6] = [1]                  
                                               
           [head^#](x1) = [1] x1 + [2]         
                                               
                  [c_7] = [1]                  
                                               
           [tail^#](x1) = [2] x1 + [2]         
                                               
                  [c_8] = [1]                  
                                               
        [sel^#](x1, x2) = [2] x1 + [2] x2 + [1]
                                               
              [c_9](x1) = [1] x1 + [2]         
                                               
   [afterNth^#](x1, x2) = [2] x1 + [2] x2 + [1]
                                               
             [c_10](x1) = [1] x1 + [2]         
                                               
       [take^#](x1, x2) = [2] x1 + [2] x2 + [1]
                                               
             [c_11](x1) = [1] x1 + [2]         

This order satisfies following ordering constraints:

           [snd(pair(XS, YS))] = [1] YS + [3]                 
                               > [1] YS + [0]                 
                               = [YS]                         
                                                              
  [splitAt(s(N), cons(X, XS))] = [2] N + [2] XS + [2] X + [4] 
                               > [2] N + [2] XS + [1] X + [2] 
                               = [u(splitAt(N, XS), N, X, XS)]
                                                              
            [splitAt(0(), XS)] = [2] XS + [4]                 
                               > [1] XS + [2]                 
                               = [pair(nil(), XS)]            
                                                              
   [u(pair(YS, ZS), N, X, XS)] = [1] X + [1] ZS + [4]         
                               > [1] ZS + [2]                 
                               = [pair(cons(X, YS), ZS)]      
                                                              
             [afterNth(N, XS)] = [2] N + [2] XS + [2]         
                               > [2] N + [2] XS + [1]         
                               = [snd(splitAt(N, XS))]        
                                                              

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
  , afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
  , take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Weak DPs:
  { fst^#(pair(XS, YS)) -> c_2()
  , snd^#(pair(XS, YS)) -> c_3()
  , splitAt^#(s(N), cons(X, XS)) ->
    c_4(u^#(splitAt(N, XS), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , u^#(pair(YS, ZS), N, X, XS) -> c_6()
  , head^#(cons(N, XS)) -> c_7()
  , tail^#(cons(N, XS)) -> c_8() }
Weak Trs:
  { snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
  , afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {2,3,4} by applications of
Pre({2,3,4}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
    , 2: sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
    , 3: afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
    , 4: take^#(N, XS) -> c_11(fst^#(splitAt(N, XS)))
    , 5: fst^#(pair(XS, YS)) -> c_2()
    , 6: snd^#(pair(XS, YS)) -> c_3()
    , 7: splitAt^#(s(N), cons(X, XS)) ->
         c_4(u^#(splitAt(N, XS), N, X, XS))
    , 8: splitAt^#(0(), XS) -> c_5()
    , 9: u^#(pair(YS, ZS), N, X, XS) -> c_6()
    , 10: head^#(cons(N, XS)) -> c_7()
    , 11: tail^#(cons(N, XS)) -> c_8() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs: { natsFrom^#(N) -> c_1(natsFrom^#(s(N))) }
Weak DPs:
  { fst^#(pair(XS, YS)) -> c_2()
  , snd^#(pair(XS, YS)) -> c_3()
  , splitAt^#(s(N), cons(X, XS)) ->
    c_4(u^#(splitAt(N, XS), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , u^#(pair(YS, ZS), N, X, XS) -> c_6()
  , head^#(cons(N, XS)) -> c_7()
  , tail^#(cons(N, XS)) -> c_8()
  , sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
  , afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
  , take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Weak Trs:
  { snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
  , afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
  c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8()
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs: { natsFrom^#(N) -> c_1(natsFrom^#(s(N))) }
Weak Trs:
  { snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
  , afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs: { natsFrom^#(N) -> c_1(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..