YES

We show the termination of the TRS R:

  a__natsFrom(N) -> cons(mark(N),natsFrom(s(N)))
  a__fst(pair(XS,YS)) -> mark(XS)
  a__snd(pair(XS,YS)) -> mark(YS)
  a__splitAt(|0|(),XS) -> pair(nil(),mark(XS))
  a__splitAt(s(N),cons(X,XS)) -> a__u(a__splitAt(mark(N),mark(XS)),N,X,XS)
  a__u(pair(YS,ZS),N,X,XS) -> pair(cons(mark(X),YS),mark(ZS))
  a__head(cons(N,XS)) -> mark(N)
  a__tail(cons(N,XS)) -> mark(XS)
  a__sel(N,XS) -> a__head(a__afterNth(mark(N),mark(XS)))
  a__take(N,XS) -> a__fst(a__splitAt(mark(N),mark(XS)))
  a__afterNth(N,XS) -> a__snd(a__splitAt(mark(N),mark(XS)))
  mark(natsFrom(X)) -> a__natsFrom(mark(X))
  mark(fst(X)) -> a__fst(mark(X))
  mark(snd(X)) -> a__snd(mark(X))
  mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2))
  mark(u(X1,X2,X3,X4)) -> a__u(mark(X1),X2,X3,X4)
  mark(head(X)) -> a__head(mark(X))
  mark(tail(X)) -> a__tail(mark(X))
  mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2))
  mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2))
  mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
  mark(cons(X1,X2)) -> cons(mark(X1),X2)
  mark(s(X)) -> s(mark(X))
  mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
  mark(|0|()) -> |0|()
  mark(nil()) -> nil()
  a__natsFrom(X) -> natsFrom(X)
  a__fst(X) -> fst(X)
  a__snd(X) -> snd(X)
  a__splitAt(X1,X2) -> splitAt(X1,X2)
  a__u(X1,X2,X3,X4) -> u(X1,X2,X3,X4)
  a__head(X) -> head(X)
  a__tail(X) -> tail(X)
  a__sel(X1,X2) -> sel(X1,X2)
  a__afterNth(X1,X2) -> afterNth(X1,X2)
  a__take(X1,X2) -> take(X1,X2)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a__natsFrom#(N) -> mark#(N)
p2: a__fst#(pair(XS,YS)) -> mark#(XS)
p3: a__snd#(pair(XS,YS)) -> mark#(YS)
p4: a__splitAt#(|0|(),XS) -> mark#(XS)
p5: a__splitAt#(s(N),cons(X,XS)) -> a__u#(a__splitAt(mark(N),mark(XS)),N,X,XS)
p6: a__splitAt#(s(N),cons(X,XS)) -> a__splitAt#(mark(N),mark(XS))
p7: a__splitAt#(s(N),cons(X,XS)) -> mark#(N)
p8: a__splitAt#(s(N),cons(X,XS)) -> mark#(XS)
p9: a__u#(pair(YS,ZS),N,X,XS) -> mark#(X)
p10: a__u#(pair(YS,ZS),N,X,XS) -> mark#(ZS)
p11: a__head#(cons(N,XS)) -> mark#(N)
p12: a__tail#(cons(N,XS)) -> mark#(XS)
p13: a__sel#(N,XS) -> a__head#(a__afterNth(mark(N),mark(XS)))
p14: a__sel#(N,XS) -> a__afterNth#(mark(N),mark(XS))
p15: a__sel#(N,XS) -> mark#(N)
p16: a__sel#(N,XS) -> mark#(XS)
p17: a__take#(N,XS) -> a__fst#(a__splitAt(mark(N),mark(XS)))
p18: a__take#(N,XS) -> a__splitAt#(mark(N),mark(XS))
p19: a__take#(N,XS) -> mark#(N)
p20: a__take#(N,XS) -> mark#(XS)
p21: a__afterNth#(N,XS) -> a__snd#(a__splitAt(mark(N),mark(XS)))
p22: a__afterNth#(N,XS) -> a__splitAt#(mark(N),mark(XS))
p23: a__afterNth#(N,XS) -> mark#(N)
p24: a__afterNth#(N,XS) -> mark#(XS)
p25: mark#(natsFrom(X)) -> a__natsFrom#(mark(X))
p26: mark#(natsFrom(X)) -> mark#(X)
p27: mark#(fst(X)) -> a__fst#(mark(X))
p28: mark#(fst(X)) -> mark#(X)
p29: mark#(snd(X)) -> a__snd#(mark(X))
p30: mark#(snd(X)) -> mark#(X)
p31: mark#(splitAt(X1,X2)) -> a__splitAt#(mark(X1),mark(X2))
p32: mark#(splitAt(X1,X2)) -> mark#(X1)
p33: mark#(splitAt(X1,X2)) -> mark#(X2)
p34: mark#(u(X1,X2,X3,X4)) -> a__u#(mark(X1),X2,X3,X4)
p35: mark#(u(X1,X2,X3,X4)) -> mark#(X1)
p36: mark#(head(X)) -> a__head#(mark(X))
p37: mark#(head(X)) -> mark#(X)
p38: mark#(tail(X)) -> a__tail#(mark(X))
p39: mark#(tail(X)) -> mark#(X)
p40: mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2))
p41: mark#(sel(X1,X2)) -> mark#(X1)
p42: mark#(sel(X1,X2)) -> mark#(X2)
p43: mark#(afterNth(X1,X2)) -> a__afterNth#(mark(X1),mark(X2))
p44: mark#(afterNth(X1,X2)) -> mark#(X1)
p45: mark#(afterNth(X1,X2)) -> mark#(X2)
p46: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p47: mark#(take(X1,X2)) -> mark#(X1)
p48: mark#(take(X1,X2)) -> mark#(X2)
p49: mark#(cons(X1,X2)) -> mark#(X1)
p50: mark#(s(X)) -> mark#(X)
p51: mark#(pair(X1,X2)) -> mark#(X1)
p52: mark#(pair(X1,X2)) -> mark#(X2)

and R consists of:

r1: a__natsFrom(N) -> cons(mark(N),natsFrom(s(N)))
r2: a__fst(pair(XS,YS)) -> mark(XS)
r3: a__snd(pair(XS,YS)) -> mark(YS)
r4: a__splitAt(|0|(),XS) -> pair(nil(),mark(XS))
r5: a__splitAt(s(N),cons(X,XS)) -> a__u(a__splitAt(mark(N),mark(XS)),N,X,XS)
r6: a__u(pair(YS,ZS),N,X,XS) -> pair(cons(mark(X),YS),mark(ZS))
r7: a__head(cons(N,XS)) -> mark(N)
r8: a__tail(cons(N,XS)) -> mark(XS)
r9: a__sel(N,XS) -> a__head(a__afterNth(mark(N),mark(XS)))
r10: a__take(N,XS) -> a__fst(a__splitAt(mark(N),mark(XS)))
r11: a__afterNth(N,XS) -> a__snd(a__splitAt(mark(N),mark(XS)))
r12: mark(natsFrom(X)) -> a__natsFrom(mark(X))
r13: mark(fst(X)) -> a__fst(mark(X))
r14: mark(snd(X)) -> a__snd(mark(X))
r15: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2))
r16: mark(u(X1,X2,X3,X4)) -> a__u(mark(X1),X2,X3,X4)
r17: mark(head(X)) -> a__head(mark(X))
r18: mark(tail(X)) -> a__tail(mark(X))
r19: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2))
r20: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2))
r21: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r22: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r23: mark(s(X)) -> s(mark(X))
r24: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r25: mark(|0|()) -> |0|()
r26: mark(nil()) -> nil()
r27: a__natsFrom(X) -> natsFrom(X)
r28: a__fst(X) -> fst(X)
r29: a__snd(X) -> snd(X)
r30: a__splitAt(X1,X2) -> splitAt(X1,X2)
r31: a__u(X1,X2,X3,X4) -> u(X1,X2,X3,X4)
r32: a__head(X) -> head(X)
r33: a__tail(X) -> tail(X)
r34: a__sel(X1,X2) -> sel(X1,X2)
r35: a__afterNth(X1,X2) -> afterNth(X1,X2)
r36: a__take(X1,X2) -> take(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46, p47, p48, p49, p50, p51, p52}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__natsFrom#(N) -> mark#(N)
p2: mark#(pair(X1,X2)) -> mark#(X2)
p3: mark#(pair(X1,X2)) -> mark#(X1)
p4: mark#(s(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> mark#(X1)
p6: mark#(take(X1,X2)) -> mark#(X2)
p7: mark#(take(X1,X2)) -> mark#(X1)
p8: mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
p9: a__take#(N,XS) -> mark#(XS)
p10: mark#(afterNth(X1,X2)) -> mark#(X2)
p11: mark#(afterNth(X1,X2)) -> mark#(X1)
p12: mark#(afterNth(X1,X2)) -> a__afterNth#(mark(X1),mark(X2))
p13: a__afterNth#(N,XS) -> mark#(XS)
p14: mark#(sel(X1,X2)) -> mark#(X2)
p15: mark#(sel(X1,X2)) -> mark#(X1)
p16: mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2))
p17: a__sel#(N,XS) -> mark#(XS)
p18: mark#(tail(X)) -> mark#(X)
p19: mark#(tail(X)) -> a__tail#(mark(X))
p20: a__tail#(cons(N,XS)) -> mark#(XS)
p21: mark#(head(X)) -> mark#(X)
p22: mark#(head(X)) -> a__head#(mark(X))
p23: a__head#(cons(N,XS)) -> mark#(N)
p24: mark#(u(X1,X2,X3,X4)) -> mark#(X1)
p25: mark#(u(X1,X2,X3,X4)) -> a__u#(mark(X1),X2,X3,X4)
p26: a__u#(pair(YS,ZS),N,X,XS) -> mark#(ZS)
p27: mark#(splitAt(X1,X2)) -> mark#(X2)
p28: mark#(splitAt(X1,X2)) -> mark#(X1)
p29: mark#(splitAt(X1,X2)) -> a__splitAt#(mark(X1),mark(X2))
p30: a__splitAt#(s(N),cons(X,XS)) -> mark#(XS)
p31: mark#(snd(X)) -> mark#(X)
p32: mark#(snd(X)) -> a__snd#(mark(X))
p33: a__snd#(pair(XS,YS)) -> mark#(YS)
p34: mark#(fst(X)) -> mark#(X)
p35: mark#(fst(X)) -> a__fst#(mark(X))
p36: a__fst#(pair(XS,YS)) -> mark#(XS)
p37: mark#(natsFrom(X)) -> mark#(X)
p38: mark#(natsFrom(X)) -> a__natsFrom#(mark(X))
p39: a__splitAt#(s(N),cons(X,XS)) -> mark#(N)
p40: a__splitAt#(s(N),cons(X,XS)) -> a__splitAt#(mark(N),mark(XS))
p41: a__splitAt#(s(N),cons(X,XS)) -> a__u#(a__splitAt(mark(N),mark(XS)),N,X,XS)
p42: a__u#(pair(YS,ZS),N,X,XS) -> mark#(X)
p43: a__splitAt#(|0|(),XS) -> mark#(XS)
p44: a__sel#(N,XS) -> mark#(N)
p45: a__sel#(N,XS) -> a__afterNth#(mark(N),mark(XS))
p46: a__afterNth#(N,XS) -> mark#(N)
p47: a__afterNth#(N,XS) -> a__splitAt#(mark(N),mark(XS))
p48: a__afterNth#(N,XS) -> a__snd#(a__splitAt(mark(N),mark(XS)))
p49: a__sel#(N,XS) -> a__head#(a__afterNth(mark(N),mark(XS)))
p50: a__take#(N,XS) -> mark#(N)
p51: a__take#(N,XS) -> a__splitAt#(mark(N),mark(XS))
p52: a__take#(N,XS) -> a__fst#(a__splitAt(mark(N),mark(XS)))

and R consists of:

r1: a__natsFrom(N) -> cons(mark(N),natsFrom(s(N)))
r2: a__fst(pair(XS,YS)) -> mark(XS)
r3: a__snd(pair(XS,YS)) -> mark(YS)
r4: a__splitAt(|0|(),XS) -> pair(nil(),mark(XS))
r5: a__splitAt(s(N),cons(X,XS)) -> a__u(a__splitAt(mark(N),mark(XS)),N,X,XS)
r6: a__u(pair(YS,ZS),N,X,XS) -> pair(cons(mark(X),YS),mark(ZS))
r7: a__head(cons(N,XS)) -> mark(N)
r8: a__tail(cons(N,XS)) -> mark(XS)
r9: a__sel(N,XS) -> a__head(a__afterNth(mark(N),mark(XS)))
r10: a__take(N,XS) -> a__fst(a__splitAt(mark(N),mark(XS)))
r11: a__afterNth(N,XS) -> a__snd(a__splitAt(mark(N),mark(XS)))
r12: mark(natsFrom(X)) -> a__natsFrom(mark(X))
r13: mark(fst(X)) -> a__fst(mark(X))
r14: mark(snd(X)) -> a__snd(mark(X))
r15: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2))
r16: mark(u(X1,X2,X3,X4)) -> a__u(mark(X1),X2,X3,X4)
r17: mark(head(X)) -> a__head(mark(X))
r18: mark(tail(X)) -> a__tail(mark(X))
r19: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2))
r20: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2))
r21: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r22: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r23: mark(s(X)) -> s(mark(X))
r24: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r25: mark(|0|()) -> |0|()
r26: mark(nil()) -> nil()
r27: a__natsFrom(X) -> natsFrom(X)
r28: a__fst(X) -> fst(X)
r29: a__snd(X) -> snd(X)
r30: a__splitAt(X1,X2) -> splitAt(X1,X2)
r31: a__u(X1,X2,X3,X4) -> u(X1,X2,X3,X4)
r32: a__head(X) -> head(X)
r33: a__tail(X) -> tail(X)
r34: a__sel(X1,X2) -> sel(X1,X2)
r35: a__afterNth(X1,X2) -> afterNth(X1,X2)
r36: a__take(X1,X2) -> take(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__natsFrom#_A(x1) = max{67, x1 + 38}
          mark#_A(x1) = max{10, x1 + 8}
          pair_A(x1,x2) = max{113, x1 + 46, x2 + 25}
          s_A(x1) = max{21, x1}
          cons_A(x1,x2) = max{29, x1 + 9, x2}
          take_A(x1,x2) = max{331, x1 + 217, x2 + 310}
          a__take#_A(x1,x2) = max{x1 + 111, x2 + 204}
          mark_A(x1) = max{20, x1}
          afterNth_A(x1,x2) = max{188, x1 + 134, x2 + 155}
          a__afterNth#_A(x1,x2) = max{133, x1 + 113, x2 + 94}
          sel_A(x1,x2) = max{263, x1 + 221, x2 + 242}
          a__sel#_A(x1,x2) = max{x1 + 146, x2 + 200}
          tail_A(x1) = max{51, x1 + 31}
          a__tail#_A(x1) = x1 + 10
          head_A(x1) = max{42, x1 + 21}
          a__head#_A(x1) = max{30, x1 + 11}
          u_A(x1,x2,x3,x4) = max{x1, x2 + 2, x3 + 76, x4 + 86}
          a__u#_A(x1,x2,x3,x4) = max{85, x1 - 14, x2, x3 + 10, x4}
          splitAt_A(x1,x2) = max{112, x1 + 20, x2 + 87}
          a__splitAt#_A(x1,x2) = max{110, x1 + 8, x2 + 94}
          snd_A(x1) = x1
          a__snd#_A(x1) = max{0, x1 - 17}
          fst_A(x1) = max{217, x1 + 197}
          a__fst#_A(x1) = max{204, x1 + 91}
          natsFrom_A(x1) = max{59, x1 + 30}
          a__splitAt_A(x1,x2) = max{112, x1 + 20, x2 + 87}
          |0|_A = 114
          a__afterNth_A(x1,x2) = max{188, x1 + 134, x2 + 155}
          a__natsFrom_A(x1) = max{59, x1 + 30}
          a__fst_A(x1) = max{217, x1 + 197}
          a__snd_A(x1) = x1
          a__u_A(x1,x2,x3,x4) = max{x1, x2 + 2, x3 + 76, x4 + 86}
          a__head_A(x1) = max{42, x1 + 21}
          a__tail_A(x1) = max{51, x1 + 31}
          a__sel_A(x1,x2) = max{263, x1 + 221, x2 + 242}
          a__take_A(x1,x2) = max{331, x1 + 217, x2 + 310}
          nil_A = 87
    
      precedence:
      
        a__tail# = a__head# > take = a__snd# = |0| = a__take > a__afterNth# > fst = a__fst > afterNth = a__afterNth = nil > s = mark = a__splitAt# = a__snd = a__sel > mark# > a__take# = a__head > a__fst# > a__natsFrom# > head = splitAt = a__splitAt > a__u > u > a__u# > sel = a__sel# = tail = a__tail > a__natsFrom > pair = cons = snd = natsFrom
      
      partial status:
    
        pi(a__natsFrom#) = []
        pi(mark#) = []
        pi(pair) = [1]
        pi(s) = []
        pi(cons) = [1, 2]
        pi(take) = []
        pi(a__take#) = [1, 2]
        pi(mark) = [1]
        pi(afterNth) = []
        pi(a__afterNth#) = [2]
        pi(sel) = []
        pi(a__sel#) = []
        pi(tail) = []
        pi(a__tail#) = [1]
        pi(head) = []
        pi(a__head#) = [1]
        pi(u) = [2, 3]
        pi(a__u#) = [2, 3, 4]
        pi(splitAt) = []
        pi(a__splitAt#) = []
        pi(snd) = []
        pi(a__snd#) = []
        pi(fst) = []
        pi(a__fst#) = []
        pi(natsFrom) = []
        pi(a__splitAt) = [1]
        pi(|0|) = []
        pi(a__afterNth) = []
        pi(a__natsFrom) = []
        pi(a__fst) = []
        pi(a__snd) = []
        pi(a__u) = [2, 3, 4]
        pi(a__head) = []
        pi(a__tail) = []
        pi(a__sel) = []
        pi(a__take) = []
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__natsFrom#_A(x1) = 220
          mark#_A(x1) = 220
          pair_A(x1,x2) = max{346, x1 + 60}
          s_A(x1) = 242
          cons_A(x1,x2) = max{x1 + 250, x2 + 252}
          take_A(x1,x2) = 602
          a__take#_A(x1,x2) = max{x1 + 360, x2 + 409}
          mark_A(x1) = 242
          afterNth_A(x1,x2) = 202
          a__afterNth#_A(x1,x2) = max{409, x2 - 29}
          sel_A(x1,x2) = 169
          a__sel#_A(x1,x2) = 213
          tail_A(x1) = 1
          a__tail#_A(x1) = max{221, x1 + 175}
          head_A(x1) = 204
          a__head#_A(x1) = max{212, x1 - 29}
          u_A(x1,x2,x3,x4) = 182
          a__u#_A(x1,x2,x3,x4) = max{323, x4 + 221}
          splitAt_A(x1,x2) = 154
          a__splitAt#_A(x1,x2) = 243
          snd_A(x1) = 242
          a__snd#_A(x1) = 409
          fst_A(x1) = 1
          a__fst#_A(x1) = 12
          natsFrom_A(x1) = 209
          a__splitAt_A(x1,x2) = max{242, x1 + 166}
          |0|_A = 181
          a__afterNth_A(x1,x2) = 242
          a__natsFrom_A(x1) = 210
          a__fst_A(x1) = 242
          a__snd_A(x1) = 243
          a__u_A(x1,x2,x3,x4) = 195
          a__head_A(x1) = 239
          a__tail_A(x1) = 241
          a__sel_A(x1,x2) = 240
          a__take_A(x1,x2) = 637
          nil_A = 182
    
      precedence:
      
        tail > fst = |0| > nil > a__afterNth# > a__snd > mark > a__afterNth > afterNth > a__u# = a__splitAt# = a__fst# = a__tail > a__natsFrom > take = a__take# > mark# = cons > a__sel > sel > a__sel# = a__head > s > a__tail# = a__u > a__natsFrom# = a__take > natsFrom = a__splitAt > splitAt > u > head = snd > a__head# = a__snd# > pair > a__fst
      
      partial status:
    
        pi(a__natsFrom#) = []
        pi(mark#) = []
        pi(pair) = [1]
        pi(s) = []
        pi(cons) = []
        pi(take) = []
        pi(a__take#) = [1, 2]
        pi(mark) = []
        pi(afterNth) = []
        pi(a__afterNth#) = []
        pi(sel) = []
        pi(a__sel#) = []
        pi(tail) = []
        pi(a__tail#) = []
        pi(head) = []
        pi(a__head#) = []
        pi(u) = []
        pi(a__u#) = [4]
        pi(splitAt) = []
        pi(a__splitAt#) = []
        pi(snd) = []
        pi(a__snd#) = []
        pi(fst) = []
        pi(a__fst#) = []
        pi(natsFrom) = []
        pi(a__splitAt) = []
        pi(|0|) = []
        pi(a__afterNth) = []
        pi(a__natsFrom) = []
        pi(a__fst) = []
        pi(a__snd) = []
        pi(a__u) = []
        pi(a__head) = []
        pi(a__tail) = []
        pi(a__sel) = []
        pi(a__take) = []
        pi(nil) = []
    

The next rules are strictly ordered:

  p1, p8, p9, p12, p17, p19, p20, p22, p23, p25, p29, p32, p35, p36, p38, p39, p41, p44, p45, p46, p50, p52

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(pair(X1,X2)) -> mark#(X2)
p2: mark#(pair(X1,X2)) -> mark#(X1)
p3: mark#(s(X)) -> mark#(X)
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(take(X1,X2)) -> mark#(X2)
p6: mark#(take(X1,X2)) -> mark#(X1)
p7: mark#(afterNth(X1,X2)) -> mark#(X2)
p8: mark#(afterNth(X1,X2)) -> mark#(X1)
p9: a__afterNth#(N,XS) -> mark#(XS)
p10: mark#(sel(X1,X2)) -> mark#(X2)
p11: mark#(sel(X1,X2)) -> mark#(X1)
p12: mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2))
p13: mark#(tail(X)) -> mark#(X)
p14: mark#(head(X)) -> mark#(X)
p15: mark#(u(X1,X2,X3,X4)) -> mark#(X1)
p16: a__u#(pair(YS,ZS),N,X,XS) -> mark#(ZS)
p17: mark#(splitAt(X1,X2)) -> mark#(X2)
p18: mark#(splitAt(X1,X2)) -> mark#(X1)
p19: a__splitAt#(s(N),cons(X,XS)) -> mark#(XS)
p20: mark#(snd(X)) -> mark#(X)
p21: a__snd#(pair(XS,YS)) -> mark#(YS)
p22: mark#(fst(X)) -> mark#(X)
p23: mark#(natsFrom(X)) -> mark#(X)
p24: a__splitAt#(s(N),cons(X,XS)) -> a__splitAt#(mark(N),mark(XS))
p25: a__u#(pair(YS,ZS),N,X,XS) -> mark#(X)
p26: a__splitAt#(|0|(),XS) -> mark#(XS)
p27: a__afterNth#(N,XS) -> a__splitAt#(mark(N),mark(XS))
p28: a__afterNth#(N,XS) -> a__snd#(a__splitAt(mark(N),mark(XS)))
p29: a__sel#(N,XS) -> a__head#(a__afterNth(mark(N),mark(XS)))
p30: a__take#(N,XS) -> a__splitAt#(mark(N),mark(XS))

and R consists of:

r1: a__natsFrom(N) -> cons(mark(N),natsFrom(s(N)))
r2: a__fst(pair(XS,YS)) -> mark(XS)
r3: a__snd(pair(XS,YS)) -> mark(YS)
r4: a__splitAt(|0|(),XS) -> pair(nil(),mark(XS))
r5: a__splitAt(s(N),cons(X,XS)) -> a__u(a__splitAt(mark(N),mark(XS)),N,X,XS)
r6: a__u(pair(YS,ZS),N,X,XS) -> pair(cons(mark(X),YS),mark(ZS))
r7: a__head(cons(N,XS)) -> mark(N)
r8: a__tail(cons(N,XS)) -> mark(XS)
r9: a__sel(N,XS) -> a__head(a__afterNth(mark(N),mark(XS)))
r10: a__take(N,XS) -> a__fst(a__splitAt(mark(N),mark(XS)))
r11: a__afterNth(N,XS) -> a__snd(a__splitAt(mark(N),mark(XS)))
r12: mark(natsFrom(X)) -> a__natsFrom(mark(X))
r13: mark(fst(X)) -> a__fst(mark(X))
r14: mark(snd(X)) -> a__snd(mark(X))
r15: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2))
r16: mark(u(X1,X2,X3,X4)) -> a__u(mark(X1),X2,X3,X4)
r17: mark(head(X)) -> a__head(mark(X))
r18: mark(tail(X)) -> a__tail(mark(X))
r19: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2))
r20: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2))
r21: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r22: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r23: mark(s(X)) -> s(mark(X))
r24: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r25: mark(|0|()) -> |0|()
r26: mark(nil()) -> nil()
r27: a__natsFrom(X) -> natsFrom(X)
r28: a__fst(X) -> fst(X)
r29: a__snd(X) -> snd(X)
r30: a__splitAt(X1,X2) -> splitAt(X1,X2)
r31: a__u(X1,X2,X3,X4) -> u(X1,X2,X3,X4)
r32: a__head(X) -> head(X)
r33: a__tail(X) -> tail(X)
r34: a__sel(X1,X2) -> sel(X1,X2)
r35: a__afterNth(X1,X2) -> afterNth(X1,X2)
r36: a__take(X1,X2) -> take(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p24}
  {p1, p2, p3, p4, p5, p6, p7, p8, p10, p11, p13, p14, p15, p17, p18, p20, p22, p23}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__splitAt#(s(N),cons(X,XS)) -> a__splitAt#(mark(N),mark(XS))

and R consists of:

r1: a__natsFrom(N) -> cons(mark(N),natsFrom(s(N)))
r2: a__fst(pair(XS,YS)) -> mark(XS)
r3: a__snd(pair(XS,YS)) -> mark(YS)
r4: a__splitAt(|0|(),XS) -> pair(nil(),mark(XS))
r5: a__splitAt(s(N),cons(X,XS)) -> a__u(a__splitAt(mark(N),mark(XS)),N,X,XS)
r6: a__u(pair(YS,ZS),N,X,XS) -> pair(cons(mark(X),YS),mark(ZS))
r7: a__head(cons(N,XS)) -> mark(N)
r8: a__tail(cons(N,XS)) -> mark(XS)
r9: a__sel(N,XS) -> a__head(a__afterNth(mark(N),mark(XS)))
r10: a__take(N,XS) -> a__fst(a__splitAt(mark(N),mark(XS)))
r11: a__afterNth(N,XS) -> a__snd(a__splitAt(mark(N),mark(XS)))
r12: mark(natsFrom(X)) -> a__natsFrom(mark(X))
r13: mark(fst(X)) -> a__fst(mark(X))
r14: mark(snd(X)) -> a__snd(mark(X))
r15: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2))
r16: mark(u(X1,X2,X3,X4)) -> a__u(mark(X1),X2,X3,X4)
r17: mark(head(X)) -> a__head(mark(X))
r18: mark(tail(X)) -> a__tail(mark(X))
r19: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2))
r20: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2))
r21: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r22: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r23: mark(s(X)) -> s(mark(X))
r24: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r25: mark(|0|()) -> |0|()
r26: mark(nil()) -> nil()
r27: a__natsFrom(X) -> natsFrom(X)
r28: a__fst(X) -> fst(X)
r29: a__snd(X) -> snd(X)
r30: a__splitAt(X1,X2) -> splitAt(X1,X2)
r31: a__u(X1,X2,X3,X4) -> u(X1,X2,X3,X4)
r32: a__head(X) -> head(X)
r33: a__tail(X) -> tail(X)
r34: a__sel(X1,X2) -> sel(X1,X2)
r35: a__afterNth(X1,X2) -> afterNth(X1,X2)
r36: a__take(X1,X2) -> take(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__splitAt#_A(x1,x2) = max{x1 + 2, x2 + 2}
          s_A(x1) = x1
          cons_A(x1,x2) = max{x1, x2}
          mark_A(x1) = x1
          a__natsFrom_A(x1) = x1
          natsFrom_A(x1) = x1
          a__fst_A(x1) = max{9, x1 + 3}
          pair_A(x1,x2) = max{0, x1 - 1, x2 - 2}
          a__snd_A(x1) = max{8, x1 + 3}
          a__splitAt_A(x1,x2) = max{x1 + 5, x2}
          |0|_A = 1
          nil_A = 0
          a__u_A(x1,x2,x3,x4) = max{x1, x2 + 5, x3, x4}
          a__head_A(x1) = max{14, x1 + 3}
          a__tail_A(x1) = max{2, x1 + 1}
          a__sel_A(x1,x2) = max{16, x1 + 15, x2 + 12}
          a__afterNth_A(x1,x2) = max{x1 + 11, x2 + 9}
          a__take_A(x1,x2) = max{x1 + 9, x2 + 3}
          fst_A(x1) = max{9, x1 + 3}
          snd_A(x1) = max{8, x1 + 3}
          splitAt_A(x1,x2) = max{x1 + 5, x2}
          u_A(x1,x2,x3,x4) = max{x1, x2 + 5, x3, x4}
          head_A(x1) = max{14, x1 + 3}
          tail_A(x1) = max{2, x1 + 1}
          sel_A(x1,x2) = max{16, x1 + 15, x2 + 12}
          afterNth_A(x1,x2) = max{x1 + 11, x2 + 9}
          take_A(x1,x2) = max{x1 + 9, x2 + 3}
    
      precedence:
      
        a__splitAt# = |0| = a__tail = tail > s = mark = a__sel = sel > a__natsFrom > a__splitAt > a__snd = splitAt > natsFrom > a__fst = a__take > a__head > a__afterNth = afterNth = take > head > a__u > cons = pair = nil = fst = snd = u
      
      partial status:
    
        pi(a__splitAt#) = [1]
        pi(s) = [1]
        pi(cons) = []
        pi(mark) = [1]
        pi(a__natsFrom) = [1]
        pi(natsFrom) = [1]
        pi(a__fst) = []
        pi(pair) = []
        pi(a__snd) = []
        pi(a__splitAt) = [1, 2]
        pi(|0|) = []
        pi(nil) = []
        pi(a__u) = [2]
        pi(a__head) = [1]
        pi(a__tail) = []
        pi(a__sel) = [2]
        pi(a__afterNth) = []
        pi(a__take) = [2]
        pi(fst) = []
        pi(snd) = []
        pi(splitAt) = [1, 2]
        pi(u) = []
        pi(head) = [1]
        pi(tail) = []
        pi(sel) = []
        pi(afterNth) = []
        pi(take) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__splitAt#_A(x1,x2) = max{35, x1}
          s_A(x1) = max{76, x1 + 41}
          cons_A(x1,x2) = 49
          mark_A(x1) = max{34, x1 + 24}
          a__natsFrom_A(x1) = 50
          natsFrom_A(x1) = 33
          a__fst_A(x1) = 2
          pair_A(x1,x2) = 7
          a__snd_A(x1) = 35
          a__splitAt_A(x1,x2) = 34
          |0|_A = 61
          nil_A = 60
          a__u_A(x1,x2,x3,x4) = 34
          a__head_A(x1) = max{26, x1 - 15}
          a__tail_A(x1) = 35
          a__sel_A(x1,x2) = 34
          a__afterNth_A(x1,x2) = 34
          a__take_A(x1,x2) = max{37, x2 + 3}
          fst_A(x1) = 1
          snd_A(x1) = 35
          splitAt_A(x1,x2) = max{33, x1 + 22, x2 + 11}
          u_A(x1,x2,x3,x4) = 0
          head_A(x1) = x1 + 1
          tail_A(x1) = 35
          sel_A(x1,x2) = 34
          afterNth_A(x1,x2) = 10
          take_A(x1,x2) = max{13, x2 + 3}
    
      precedence:
      
        mark > a__splitAt > a__splitAt# = a__fst = pair = |0| = nil = a__u = a__afterNth = fst > a__snd = a__sel = a__take = snd > a__head = afterNth = take > s = cons = a__natsFrom = natsFrom = a__tail = splitAt = u > head = tail = sel
      
      partial status:
    
        pi(a__splitAt#) = [1]
        pi(s) = [1]
        pi(cons) = []
        pi(mark) = [1]
        pi(a__natsFrom) = []
        pi(natsFrom) = []
        pi(a__fst) = []
        pi(pair) = []
        pi(a__snd) = []
        pi(a__splitAt) = []
        pi(|0|) = []
        pi(nil) = []
        pi(a__u) = []
        pi(a__head) = []
        pi(a__tail) = []
        pi(a__sel) = []
        pi(a__afterNth) = []
        pi(a__take) = []
        pi(fst) = []
        pi(snd) = []
        pi(splitAt) = [1]
        pi(u) = []
        pi(head) = []
        pi(tail) = []
        pi(sel) = []
        pi(afterNth) = []
        pi(take) = [2]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(pair(X1,X2)) -> mark#(X2)
p2: mark#(natsFrom(X)) -> mark#(X)
p3: mark#(fst(X)) -> mark#(X)
p4: mark#(snd(X)) -> mark#(X)
p5: mark#(splitAt(X1,X2)) -> mark#(X1)
p6: mark#(splitAt(X1,X2)) -> mark#(X2)
p7: mark#(u(X1,X2,X3,X4)) -> mark#(X1)
p8: mark#(head(X)) -> mark#(X)
p9: mark#(tail(X)) -> mark#(X)
p10: mark#(sel(X1,X2)) -> mark#(X1)
p11: mark#(sel(X1,X2)) -> mark#(X2)
p12: mark#(afterNth(X1,X2)) -> mark#(X1)
p13: mark#(afterNth(X1,X2)) -> mark#(X2)
p14: mark#(take(X1,X2)) -> mark#(X1)
p15: mark#(take(X1,X2)) -> mark#(X2)
p16: mark#(cons(X1,X2)) -> mark#(X1)
p17: mark#(s(X)) -> mark#(X)
p18: mark#(pair(X1,X2)) -> mark#(X1)

and R consists of:

r1: a__natsFrom(N) -> cons(mark(N),natsFrom(s(N)))
r2: a__fst(pair(XS,YS)) -> mark(XS)
r3: a__snd(pair(XS,YS)) -> mark(YS)
r4: a__splitAt(|0|(),XS) -> pair(nil(),mark(XS))
r5: a__splitAt(s(N),cons(X,XS)) -> a__u(a__splitAt(mark(N),mark(XS)),N,X,XS)
r6: a__u(pair(YS,ZS),N,X,XS) -> pair(cons(mark(X),YS),mark(ZS))
r7: a__head(cons(N,XS)) -> mark(N)
r8: a__tail(cons(N,XS)) -> mark(XS)
r9: a__sel(N,XS) -> a__head(a__afterNth(mark(N),mark(XS)))
r10: a__take(N,XS) -> a__fst(a__splitAt(mark(N),mark(XS)))
r11: a__afterNth(N,XS) -> a__snd(a__splitAt(mark(N),mark(XS)))
r12: mark(natsFrom(X)) -> a__natsFrom(mark(X))
r13: mark(fst(X)) -> a__fst(mark(X))
r14: mark(snd(X)) -> a__snd(mark(X))
r15: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2))
r16: mark(u(X1,X2,X3,X4)) -> a__u(mark(X1),X2,X3,X4)
r17: mark(head(X)) -> a__head(mark(X))
r18: mark(tail(X)) -> a__tail(mark(X))
r19: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2))
r20: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2))
r21: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
r22: mark(cons(X1,X2)) -> cons(mark(X1),X2)
r23: mark(s(X)) -> s(mark(X))
r24: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
r25: mark(|0|()) -> |0|()
r26: mark(nil()) -> nil()
r27: a__natsFrom(X) -> natsFrom(X)
r28: a__fst(X) -> fst(X)
r29: a__snd(X) -> snd(X)
r30: a__splitAt(X1,X2) -> splitAt(X1,X2)
r31: a__u(X1,X2,X3,X4) -> u(X1,X2,X3,X4)
r32: a__head(X) -> head(X)
r33: a__tail(X) -> tail(X)
r34: a__sel(X1,X2) -> sel(X1,X2)
r35: a__afterNth(X1,X2) -> afterNth(X1,X2)
r36: a__take(X1,X2) -> take(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{4, x1 + 3}
          pair_A(x1,x2) = max{x1, x2}
          natsFrom_A(x1) = max{1, x1}
          fst_A(x1) = max{3, x1 + 2}
          snd_A(x1) = max{1, x1}
          splitAt_A(x1,x2) = max{x1, x2}
          u_A(x1,x2,x3,x4) = max{x1, x2, x3, x4}
          head_A(x1) = max{1, x1}
          tail_A(x1) = max{1, x1}
          sel_A(x1,x2) = max{x1, x2}
          afterNth_A(x1,x2) = max{x1, x2}
          take_A(x1,x2) = max{1, x1, x2}
          cons_A(x1,x2) = max{x1, x2}
          s_A(x1) = max{1, x1}
    
      precedence:
      
        mark# = pair = natsFrom = fst = snd = splitAt = u = head = tail = sel = afterNth = take = cons = s
      
      partial status:
    
        pi(mark#) = [1]
        pi(pair) = [1, 2]
        pi(natsFrom) = [1]
        pi(fst) = [1]
        pi(snd) = [1]
        pi(splitAt) = [1, 2]
        pi(u) = [1, 2, 3, 4]
        pi(head) = [1]
        pi(tail) = [1]
        pi(sel) = [1, 2]
        pi(afterNth) = [1, 2]
        pi(take) = [1, 2]
        pi(cons) = [1, 2]
        pi(s) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = max{4, x1 + 3}
          pair_A(x1,x2) = max{x1 + 2, x2 + 2}
          natsFrom_A(x1) = x1 + 2
          fst_A(x1) = x1 + 2
          snd_A(x1) = x1 + 2
          splitAt_A(x1,x2) = max{x1 + 2, x2 + 2}
          u_A(x1,x2,x3,x4) = max{x1 + 2, x2 + 2, x3 + 2, x4 + 2}
          head_A(x1) = x1 + 2
          tail_A(x1) = x1 + 2
          sel_A(x1,x2) = max{x1 + 2, x2 + 2}
          afterNth_A(x1,x2) = max{x1 + 2, x2 + 2}
          take_A(x1,x2) = max{x1 + 2, x2 + 2}
          cons_A(x1,x2) = max{x1 + 4, x2 + 4}
          s_A(x1) = max{3, x1 + 2}
    
      precedence:
      
        mark# = pair = natsFrom = fst = snd = splitAt = u = head = tail = sel = afterNth = take = cons = s
      
      partial status:
    
        pi(mark#) = []
        pi(pair) = [2]
        pi(natsFrom) = [1]
        pi(fst) = [1]
        pi(snd) = [1]
        pi(splitAt) = [2]
        pi(u) = [4]
        pi(head) = [1]
        pi(tail) = [1]
        pi(sel) = [2]
        pi(afterNth) = [2]
        pi(take) = [2]
        pi(cons) = [2]
        pi(s) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18

We remove them from the problem.  Then no dependency pair remains.