We consider the system h37.

  Alphabet:

    0 : [] --> A 
    afterNth : [] --> A -> A -> A 
    and : [] --> A -> A -> A 
    axxafterNth : [] --> A -> A -> A 
    axxand : [] --> A -> A -> A 
    axxfst : [] --> A -> A 
    axxhead : [] --> A -> A 
    axxnatsFrom : [] --> A -> A 
    axxsel : [] --> A -> A -> A 
    axxsnd : [] --> A -> A 
    axxsplitAt : [] --> A -> A -> A 
    axxtail : [] --> A -> A 
    axxtake : [] --> A -> A -> A 
    axxu11 : [] --> A -> A -> A -> A -> A 
    axxu12 : [] --> A -> A -> A 
    cons : [] --> A -> A -> A 
    foldr : [] --> (A -> A -> A) -> A -> A -> A 
    fst : [] --> A -> A 
    head : [] --> A -> A 
    mark : [] --> A -> A 
    natsFrom : [] --> A -> A 
    nil : [] --> A 
    pair : [] --> A -> A -> A 
    s : [] --> A -> A 
    sel : [] --> A -> A -> A 
    snd : [] --> A -> A 
    splitAt : [] --> A -> A -> A 
    tail : [] --> A -> A 
    take : [] --> A -> A -> A 
    tt : [] --> A 
    u11 : [] --> A -> A -> A -> A -> A 
    u12 : [] --> A -> A -> A 

  Rules:

    axxu11 tt x y z => axxu12 (axxsplitAt (mark x) (mark z)) y 
    axxu12 (pair x y) z => pair (cons (mark z) x) (mark y) 
    axxafterNth x y => axxsnd (axxsplitAt (mark x) (mark y)) 
    axxand tt x => mark x 
    axxfst (pair x y) => mark x 
    axxhead (cons x y) => mark x 
    axxnatsFrom x => cons (mark x) (natsFrom (s x)) 
    axxsel x y => axxhead (axxafterNth (mark x) (mark y)) 
    axxsnd (pair x y) => mark y 
    axxsplitAt 0 x => pair nil (mark x) 
    axxsplitAt (s x) (cons y z) => axxu11 tt x y z 
    axxtail (cons x y) => mark y 
    axxtake x y => axxfst (axxsplitAt (mark x) (mark y)) 
    mark (u11 x y z u) => axxu11 (mark x) y z u 
    mark (u12 x y) => axxu12 (mark x) y 
    mark (splitAt x y) => axxsplitAt (mark x) (mark y) 
    mark (afterNth x y) => axxafterNth (mark x) (mark y) 
    mark (snd x) => axxsnd (mark x) 
    mark (and x y) => axxand (mark x) y 
    mark (fst x) => axxfst (mark x) 
    mark (head x) => axxhead (mark x) 
    mark (natsFrom x) => axxnatsFrom (mark x) 
    mark (sel x y) => axxsel (mark x) (mark y) 
    mark (tail x) => axxtail (mark x) 
    mark (take x y) => axxtake (mark x) (mark y) 
    mark tt => tt 
    mark (pair x y) => pair (mark x) (mark y) 
    mark (cons x y) => cons (mark x) y 
    mark (s x) => s (mark x) 
    mark 0 => 0 
    mark nil => nil 
    axxu11 x y z u => u11 x y z u 
    axxu12 x y => u12 x y 
    axxsplitAt x y => splitAt x y 
    axxafterNth x y => afterNth x y 
    axxsnd x => snd x 
    axxand x y => and x y 
    axxfst x => fst x 
    axxhead x => head x 
    axxnatsFrom x => natsFrom x 
    axxsel x y => sel x y 
    axxtail x => tail x 
    axxtake x y => take x y 
    foldr (/\x./\y.f x y) z nil => z 
    foldr (/\x./\y.f x y) z (cons u v) => f u (foldr (/\w./\x'.f w x') z v) 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    0 : [] --> A 
    afterNth : [A * A] --> A 
    and : [A * A] --> A 
    axxafterNth : [A * A] --> A 
    axxand : [A * A] --> A 
    axxfst : [A] --> A 
    axxhead : [A] --> A 
    axxnatsFrom : [A] --> A 
    axxsel : [A * A] --> A 
    axxsnd : [A] --> A 
    axxsplitAt : [A * A] --> A 
    axxtail : [A] --> A 
    axxtake : [A * A] --> A 
    axxu11 : [A * A * A * A] --> A 
    axxu12 : [A * A] --> A 
    cons : [A * A] --> A 
    foldr : [A -> A -> A * A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    mark : [A] --> A 
    natsFrom : [A] --> A 
    nil : [] --> A 
    pair : [A * A] --> A 
    s : [A] --> A 
    sel : [A * A] --> A 
    snd : [A] --> A 
    splitAt : [A * A] --> A 
    tail : [A] --> A 
    take : [A * A] --> A 
    tt : [] --> A 
    u11 : [A * A * A * A] --> A 
    u12 : [A * A] --> A 
    ~AP1 : [A -> A -> A * A] --> A -> A 

  Rules:

    axxu11(tt, X, Y, Z) => axxu12(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu12(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxafterNth(X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxand(tt, X) => mark(X) 
    axxfst(pair(X, Y)) => mark(X) 
    axxhead(cons(X, Y)) => mark(X) 
    axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
    axxsel(X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxsnd(pair(X, Y)) => mark(Y) 
    axxsplitAt(0, X) => pair(nil, mark(X)) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu11(tt, X, Y, Z) 
    axxtail(cons(X, Y)) => mark(Y) 
    axxtake(X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    mark(u11(X, Y, Z, U)) => axxu11(mark(X), Y, Z, U) 
    mark(u12(X, Y)) => axxu12(mark(X), Y) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(and(X, Y)) => axxand(mark(X), Y) 
    mark(fst(X)) => axxfst(mark(X)) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
    mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
    mark(tail(X)) => axxtail(mark(X)) 
    mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
    mark(tt) => tt 
    mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
    mark(cons(X, Y)) => cons(mark(X), Y) 
    mark(s(X)) => s(mark(X)) 
    mark(0) => 0 
    mark(nil) => nil 
    axxu11(X, Y, Z, U) => u11(X, Y, Z, U) 
    axxu12(X, Y) => u12(X, Y) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxsnd(X) => snd(X) 
    axxand(X, Y) => and(X, Y) 
    axxfst(X) => fst(X) 
    axxhead(X) => head(X) 
    axxnatsFrom(X) => natsFrom(X) 
    axxsel(X, Y) => sel(X, Y) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    foldr(/\x./\y.~AP1(F, x) y, X, nil) => X 
    foldr(/\x./\y.~AP1(F, x) y, X, cons(Y, Z)) => ~AP1(F, Y) foldr(/\z./\u.~AP1(F, z) u, X, Z) 
    foldr(/\x./\y.afterNth(x, y), X, nil) => X 
    foldr(/\x./\y.and(x, y), X, nil) => X 
    foldr(/\x./\y.axxafterNth(x, y), X, nil) => X 
    foldr(/\x./\y.axxand(x, y), X, nil) => X 
    foldr(/\x./\y.axxsel(x, y), X, nil) => X 
    foldr(/\x./\y.axxsplitAt(x, y), X, nil) => X 
    foldr(/\x./\y.axxtake(x, y), X, nil) => X 
    foldr(/\x./\y.axxu11(X, Y, x, y), Z, nil) => Z 
    foldr(/\x./\y.axxu12(x, y), X, nil) => X 
    foldr(/\x./\y.cons(x, y), X, nil) => X 
    foldr(/\x./\y.foldr(F, x, y), X, nil) => X 
    foldr(/\x./\y.pair(x, y), X, nil) => X 
    foldr(/\x./\y.sel(x, y), X, nil) => X 
    foldr(/\x./\y.splitAt(x, y), X, nil) => X 
    foldr(/\x./\y.take(x, y), X, nil) => X 
    foldr(/\x./\y.u11(X, Y, x, y), Z, nil) => Z 
    foldr(/\x./\y.u12(x, y), X, nil) => X 
    foldr(/\x./\y.afterNth(x, y), X, cons(Y, Z)) => afterNth(Y, foldr(/\z./\u.afterNth(z, u), X, Z)) 
    foldr(/\x./\y.and(x, y), X, cons(Y, Z)) => and(Y, foldr(/\z./\u.and(z, u), X, Z)) 
    foldr(/\x./\y.axxafterNth(x, y), X, cons(Y, Z)) => axxafterNth(Y, foldr(/\z./\u.axxafterNth(z, u), X, Z)) 
    foldr(/\x./\y.axxand(x, y), X, cons(Y, Z)) => axxand(Y, foldr(/\z./\u.axxand(z, u), X, Z)) 
    foldr(/\x./\y.axxsel(x, y), X, cons(Y, Z)) => axxsel(Y, foldr(/\z./\u.axxsel(z, u), X, Z)) 
    foldr(/\x./\y.axxsplitAt(x, y), X, cons(Y, Z)) => axxsplitAt(Y, foldr(/\z./\u.axxsplitAt(z, u), X, Z)) 
    foldr(/\x./\y.axxtake(x, y), X, cons(Y, Z)) => axxtake(Y, foldr(/\z./\u.axxtake(z, u), X, Z)) 
    foldr(/\x./\y.axxu11(X, Y, x, y), Z, cons(U, V)) => axxu11(X, Y, U, foldr(/\z./\u.axxu11(X, Y, z, u), Z, V)) 
    foldr(/\x./\y.axxu12(x, y), X, cons(Y, Z)) => axxu12(Y, foldr(/\z./\u.axxu12(z, u), X, Z)) 
    foldr(/\x./\y.cons(x, y), X, cons(Y, Z)) => cons(Y, foldr(/\z./\u.cons(z, u), X, Z)) 
    foldr(/\x./\y.foldr(F, x, y), X, cons(Y, Z)) => foldr(F, Y, foldr(/\z./\u.foldr(F, z, u), X, Z)) 
    foldr(/\x./\y.pair(x, y), X, cons(Y, Z)) => pair(Y, foldr(/\z./\u.pair(z, u), X, Z)) 
    foldr(/\x./\y.sel(x, y), X, cons(Y, Z)) => sel(Y, foldr(/\z./\u.sel(z, u), X, Z)) 
    foldr(/\x./\y.splitAt(x, y), X, cons(Y, Z)) => splitAt(Y, foldr(/\z./\u.splitAt(z, u), X, Z)) 
    foldr(/\x./\y.take(x, y), X, cons(Y, Z)) => take(Y, foldr(/\z./\u.take(z, u), X, Z)) 
    foldr(/\x./\y.u11(X, Y, x, y), Z, cons(U, V)) => u11(X, Y, U, foldr(/\z./\u.u11(X, Y, z, u), Z, V)) 
    foldr(/\x./\y.u12(x, y), X, cons(Y, Z)) => u12(Y, foldr(/\z./\u.u12(z, u), X, Z)) 
    ~AP1(F, X) => F X 

Symbol ~AP1 is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  Additionally, we can remove some (now-)redundant rules.  This gives:

  Alphabet:

    0 : [] --> A 
    afterNth : [A * A] --> A 
    and : [A * A] --> A 
    axxafterNth : [A * A] --> A 
    axxand : [A * A] --> A 
    axxfst : [A] --> A 
    axxhead : [A] --> A 
    axxnatsFrom : [A] --> A 
    axxsel : [A * A] --> A 
    axxsnd : [A] --> A 
    axxsplitAt : [A * A] --> A 
    axxtail : [A] --> A 
    axxtake : [A * A] --> A 
    axxu11 : [A * A * A * A] --> A 
    axxu12 : [A * A] --> A 
    cons : [A * A] --> A 
    foldr : [A -> A -> A * A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    mark : [A] --> A 
    natsFrom : [A] --> A 
    nil : [] --> A 
    pair : [A * A] --> A 
    s : [A] --> A 
    sel : [A * A] --> A 
    snd : [A] --> A 
    splitAt : [A * A] --> A 
    tail : [A] --> A 
    take : [A * A] --> A 
    tt : [] --> A 
    u11 : [A * A * A * A] --> A 
    u12 : [A * A] --> A 

  Rules:

    axxu11(tt, X, Y, Z) => axxu12(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu12(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxafterNth(X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxand(tt, X) => mark(X) 
    axxfst(pair(X, Y)) => mark(X) 
    axxhead(cons(X, Y)) => mark(X) 
    axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
    axxsel(X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxsnd(pair(X, Y)) => mark(Y) 
    axxsplitAt(0, X) => pair(nil, mark(X)) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu11(tt, X, Y, Z) 
    axxtail(cons(X, Y)) => mark(Y) 
    axxtake(X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    mark(u11(X, Y, Z, U)) => axxu11(mark(X), Y, Z, U) 
    mark(u12(X, Y)) => axxu12(mark(X), Y) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(and(X, Y)) => axxand(mark(X), Y) 
    mark(fst(X)) => axxfst(mark(X)) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
    mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
    mark(tail(X)) => axxtail(mark(X)) 
    mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
    mark(tt) => tt 
    mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
    mark(cons(X, Y)) => cons(mark(X), Y) 
    mark(s(X)) => s(mark(X)) 
    mark(0) => 0 
    mark(nil) => nil 
    axxu11(X, Y, Z, U) => u11(X, Y, Z, U) 
    axxu12(X, Y) => u12(X, Y) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxsnd(X) => snd(X) 
    axxand(X, Y) => and(X, Y) 
    axxfst(X) => fst(X) 
    axxhead(X) => head(X) 
    axxnatsFrom(X) => natsFrom(X) 
    axxsel(X, Y) => sel(X, Y) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    foldr(/\x./\y.X(x, y), Y, nil) => Y 
    foldr(/\x./\y.X(x, y), Y, cons(Z, U)) => X(Z, foldr(/\z./\u.X(z, u), Y, U)) 

We observe that the rules contain a first-order subset:

  axxu11(tt, X, Y, Z) => axxu12(axxsplitAt(mark(X), mark(Z)), Y) 
  axxu12(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
  axxafterNth(X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
  axxand(tt, X) => mark(X) 
  axxfst(pair(X, Y)) => mark(X) 
  axxhead(cons(X, Y)) => mark(X) 
  axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
  axxsel(X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
  axxsnd(pair(X, Y)) => mark(Y) 
  axxsplitAt(0, X) => pair(nil, mark(X)) 
  axxsplitAt(s(X), cons(Y, Z)) => axxu11(tt, X, Y, Z) 
  axxtail(cons(X, Y)) => mark(Y) 
  axxtake(X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
  mark(u11(X, Y, Z, U)) => axxu11(mark(X), Y, Z, U) 
  mark(u12(X, Y)) => axxu12(mark(X), Y) 
  mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
  mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
  mark(snd(X)) => axxsnd(mark(X)) 
  mark(and(X, Y)) => axxand(mark(X), Y) 
  mark(fst(X)) => axxfst(mark(X)) 
  mark(head(X)) => axxhead(mark(X)) 
  mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
  mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
  mark(tail(X)) => axxtail(mark(X)) 
  mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
  mark(tt) => tt 
  mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
  mark(cons(X, Y)) => cons(mark(X), Y) 
  mark(s(X)) => s(mark(X)) 
  mark(0) => 0 
  mark(nil) => nil 
  axxu11(X, Y, Z, U) => u11(X, Y, Z, U) 
  axxu12(X, Y) => u12(X, Y) 
  axxsplitAt(X, Y) => splitAt(X, Y) 
  axxafterNth(X, Y) => afterNth(X, Y) 
  axxsnd(X) => snd(X) 
  axxand(X, Y) => and(X, Y) 
  axxfst(X) => fst(X) 
  axxhead(X) => head(X) 
  axxnatsFrom(X) => natsFrom(X) 
  axxsel(X, Y) => sel(X, Y) 
  axxtail(X) => tail(X) 
  axxtake(X, Y) => take(X, Y) 

Moreover, the system is finitely branching.  Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS.

According to nattprover, this system is indeed Ce-terminating:

 || Input TRS:
 ||     1: axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu12(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY)
 ||     2: axxu12(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> pair(cons(mark(PeRCenTZ),PeRCenTX),mark(PeRCenTY))
 ||     3: axxafterNth(PeRCenTX,PeRCenTY) -> axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     4: axxand(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     5: axxfst(pair(PeRCenTX,PeRCenTY)) -> mark(PeRCenTX)
 ||     6: axxhead(cons(PeRCenTX,PeRCenTY)) -> mark(PeRCenTX)
 ||     7: axxnatsFrom(PeRCenTX) -> cons(mark(PeRCenTX),natsFrom(s(PeRCenTX)))
 ||     8: axxsel(PeRCenTX,PeRCenTY) -> axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||     9: axxsnd(pair(PeRCenTX,PeRCenTY)) -> mark(PeRCenTY)
 ||     10: axxsplitAt(0(),PeRCenTX) -> pair(nil(),mark(PeRCenTX))
 ||     11: axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     12: axxtail(cons(PeRCenTX,PeRCenTY)) -> mark(PeRCenTY)
 ||     13: axxtake(PeRCenTX,PeRCenTY) -> axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     14: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     15: mark(u12(PeRCenTX,PeRCenTY)) -> axxu12(mark(PeRCenTX),PeRCenTY)
 ||     16: mark(splitAt(PeRCenTX,PeRCenTY)) -> axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||     17: mark(afterNth(PeRCenTX,PeRCenTY)) -> axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||     18: mark(snd(PeRCenTX)) -> axxsnd(mark(PeRCenTX))
 ||     19: mark(and(PeRCenTX,PeRCenTY)) -> axxand(mark(PeRCenTX),PeRCenTY)
 ||     20: mark(fst(PeRCenTX)) -> axxfst(mark(PeRCenTX))
 ||     21: mark(head(PeRCenTX)) -> axxhead(mark(PeRCenTX))
 ||     22: mark(natsFrom(PeRCenTX)) -> axxnatsFrom(mark(PeRCenTX))
 ||     23: mark(sel(PeRCenTX,PeRCenTY)) -> axxsel(mark(PeRCenTX),mark(PeRCenTY))
 ||     24: mark(tail(PeRCenTX)) -> axxtail(mark(PeRCenTX))
 ||     25: mark(take(PeRCenTX,PeRCenTY)) -> axxtake(mark(PeRCenTX),mark(PeRCenTY))
 ||     26: mark(tt()) -> tt()
 ||     27: mark(pair(PeRCenTX,PeRCenTY)) -> pair(mark(PeRCenTX),mark(PeRCenTY))
 ||     28: mark(cons(PeRCenTX,PeRCenTY)) -> cons(mark(PeRCenTX),PeRCenTY)
 ||     29: mark(s(PeRCenTX)) -> s(mark(PeRCenTX))
 ||     30: mark(0()) -> 0()
 ||     31: mark(nil()) -> nil()
 ||     32: axxu11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     33: axxu12(PeRCenTX,PeRCenTY) -> u12(PeRCenTX,PeRCenTY)
 ||     34: axxsplitAt(PeRCenTX,PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     35: axxafterNth(PeRCenTX,PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     36: axxsnd(PeRCenTX) -> snd(PeRCenTX)
 ||     37: axxand(PeRCenTX,PeRCenTY) -> and(PeRCenTX,PeRCenTY)
 ||     38: axxfst(PeRCenTX) -> fst(PeRCenTX)
 ||     39: axxhead(PeRCenTX) -> head(PeRCenTX)
 ||     40: axxnatsFrom(PeRCenTX) -> natsFrom(PeRCenTX)
 ||     41: axxsel(PeRCenTX,PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     42: axxtail(PeRCenTX) -> tail(PeRCenTX)
 ||     43: axxtake(PeRCenTX,PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     44: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX
 ||     45: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY
 || Number of strict rules: 45
 || Direct POLO(bPol) ... failed.
 || Uncurrying ... failed.
 || Dependency Pairs:
 ||    #1: #axxu12(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTZ)
 ||    #2: #axxu12(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTY)
 ||    #3: #mark(s(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #4: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #5: #axxtake(PeRCenTX,PeRCenTY) -> #axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #6: #axxtake(PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #7: #axxtake(PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #8: #axxtake(PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #9: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #10: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #11: #mark(tail(PeRCenTX)) -> #axxtail(mark(PeRCenTX))
 ||    #12: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #13: #mark(sel(PeRCenTX,PeRCenTY)) -> #axxsel(mark(PeRCenTX),mark(PeRCenTY))
 ||    #14: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #15: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #16: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #17: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #18: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #19: #mark(take(PeRCenTX,PeRCenTY)) -> #axxtake(mark(PeRCenTX),mark(PeRCenTY))
 ||    #20: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #21: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #22: #mark(fst(PeRCenTX)) -> #axxfst(mark(PeRCenTX))
 ||    #23: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #24: #axxnatsFrom(PeRCenTX) -> #mark(PeRCenTX)
 ||    #25: #axxsplitAt(0(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #26: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #27: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #28: #mark(natsFrom(PeRCenTX)) -> #axxnatsFrom(mark(PeRCenTX))
 ||    #29: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #30: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #31: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #32: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #33: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #34: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #35: #mark(and(PeRCenTX,PeRCenTY)) -> #axxand(mark(PeRCenTX),PeRCenTY)
 ||    #36: #mark(and(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #37: #mark(head(PeRCenTX)) -> #axxhead(mark(PeRCenTX))
 ||    #38: #mark(head(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #39: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #40: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #41: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #42: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #43: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #44: #axxafterNth(PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #45: #axxafterNth(PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #46: #axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu12(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY)
 ||    #47: #axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ))
 ||    #48: #axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTX)
 ||    #49: #axxu11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTZ)
 ||    #50: #axxsel(PeRCenTX,PeRCenTY) -> #axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #51: #axxsel(PeRCenTX,PeRCenTY) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #52: #axxsel(PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #53: #axxsel(PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #54: #mark(u12(PeRCenTX,PeRCenTY)) -> #axxu12(mark(PeRCenTX),PeRCenTY)
 ||    #55: #mark(u12(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #56: #axxand(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #57: #mark(snd(PeRCenTX)) -> #axxsnd(mark(PeRCenTX))
 ||    #58: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX)
 || Number of SCCs: 1, DPs: 58
 ||   SCC { #1..58 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1
 ||       #axxu12	w: max(x1 + 1, x2 + 10)
 ||       axxsnd	w: x1 + 1
 ||       axxu11	w: max(x1 + 14, x2 + 12, x3 + 13, x4 + 11)
 ||       take	w: max(x1 + 13, x2 + 12)
 ||       and	w: max(x1 + 2, x2 + 3)
 ||       axxsplitAt	w: max(x1 + 12, x2 + 11)
 ||       pair	w: max(x1 + 9, x2 + 11)
 ||       fst	w: x1 + 1
 ||       axxand	w: max(x1 + 2, x2 + 3)
 ||       natsFrom	w: x1 + 4
 ||       splitAt	w: max(x1 + 12, x2 + 11)
 ||       #axxu11	w: max(x1 + 18, x2 + 14, x3 + 19, x4 + 15)
 ||       #axxsplitAt	w: max(x1 + 14, x2 + 15)
 ||       axxnatsFrom	w: x1 + 4
 ||       tail	w: x1 + 2
 ||       #axxafterNth	w: max(x1 + 16, x2 + 16)
 ||       #mark	w: x1 + 9
 ||       #axxtail	w: x1 + 10
 ||       0 	w: 1
 ||       #axxnatsFrom	w: x1 + 10
 ||       u11	w: max(x1 + 14, x2 + 12, x3 + 13, x4 + 11)
 ||       sel	w: max(x1 + 17, x2 + 16)
 ||       afterNth	w: max(x1 + 13, x2 + 12)
 ||       nil	w: 3
 ||       #axxsnd	w: x1 + 1
 ||       #TIlDePAIR	w: 0
 ||       axxafterNth	w: max(x1 + 13, x2 + 12)
 ||       mark	w: x1
 ||       u12	w: max(x1, x2 + 13)
 ||       axxsel	w: max(x1 + 17, x2 + 16)
 ||       axxfst	w: x1 + 1
 ||       #axxand	w: max(x2 + 10)
 ||       #axxsel	w: max(x1 + 24, x2 + 24)
 ||       head	w: x1 + 4
 ||       cons	w: max(x1 + 4, x2)
 ||       snd	w: x1 + 1
 ||       axxu12	w: max(x1, x2 + 13)
 ||       axxtail	w: x1 + 2
 ||       tt	w: 1
 ||       axxtake	w: max(x1 + 13, x2 + 12)
 ||       #axxfst	w: x1 + 1
 ||       #axxtake	w: max(x1 + 16, x2 + 16)
 ||       #axxhead	w: x1 + 10
 ||       axxhead	w: x1 + 4
 ||     USABLE RULES: { 1..43 }
 ||     Removed DPs: #1 #2 #4..9 #11..46 #48..54 #56..58
 || Number of SCCs: 2, DPs: 4
 ||   SCC { #3 #55 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1 + 1
 ||       #axxu12	w: 4
 ||       axxsnd	w: 2
 ||       axxu11	w: 0
 ||       take	w: x1 + 1
 ||       and	w: 1
 ||       axxsplitAt	w: x1
 ||       pair	w: 4
 ||       fst	w: 1
 ||       axxand	w: 3
 ||       natsFrom	w: x1 + 4
 ||       splitAt	w: 1
 ||       #axxu11	w: 4
 ||       #axxsplitAt	w: 4
 ||       axxnatsFrom	w: 3
 ||       tail	w: 4
 ||       #axxafterNth	w: 4
 ||       #mark	w: x1 + 4
 ||       #axxtail	w: 4
 ||       0 	w: 4
 ||       #axxnatsFrom	w: 4
 ||       u11	w: x1 + x2 + x4 + 1
 ||       sel	w: 5
 ||       afterNth	w: 1
 ||       nil	w: 4
 ||       #axxsnd	w: 4
 ||       #TIlDePAIR	w: 0
 ||       axxafterNth	w: 1
 ||       mark	w: 3
 ||       u12	w: x1 + 2
 ||       axxsel	w: 4
 ||       axxfst	w: 1
 ||       #axxand	w: 4
 ||       #axxsel	w: 4
 ||       head	w: 5
 ||       cons	w: x1 + x2 + 1
 ||       snd	w: 2
 ||       axxu12	w: 1
 ||       axxtail	w: 4
 ||       tt	w: 4
 ||       axxtake	w: 0
 ||       #axxfst	w: 4
 ||       #axxtake	w: 4
 ||       #axxhead	w: 0
 ||       axxhead	w: 4
 ||     USABLE RULES: { }
 ||     Removed DPs: #3 #55
 || Number of SCCs: 1, DPs: 2
 ||   SCC { #10 #47 }
 || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded.
 ||       TIlDePAIR	s: [2,1]	p: 0	w: x1 + x2
 ||       s 	s: [1]	p: 6	w: x1
 ||       #axxu12	s: []	p: 0	w: x1
 ||       axxsnd	s: []	p: 0	w: x1 + 1
 ||       axxu11	s: []	p: 2	w: max(x3 + 3, x4 + 4)
 ||       take	s: []	p: 4	w: x2 + 6
 ||       and	s: []	p: 3	w: x2 + 1
 ||       axxsplitAt	s: []	p: 5	w: max(x2 + 4)
 ||       pair	s: [2]	p: 0	w: max(x1, x2 + 2)
 ||       fst	s: []	p: 3	w: x1 + 1
 ||       axxand	s: []	p: 3	w: x2 + 1
 ||       natsFrom	s: []	p: 7	w: x1 + 2
 ||       splitAt	s: []	p: 5	w: max(x2 + 4)
 ||       #axxu11	s: [2]	p: 5	w: max(x2)
 ||       #axxsplitAt	s: [1]	p: 3	w: max(x1)
 ||       axxnatsFrom	s: []	p: 7	w: x1 + 2
 ||       tail	s: [1]	p: 3	w: x1 + 1
 ||       #axxafterNth	s: [2]	p: 0	w: x2 + 1
 ||       #mark	s: []	p: 0	w: 1
 ||       #axxtail	s: []	p: 0	w: 1
 ||       0 	s: []	p: 4	w: 1
 ||       #axxnatsFrom	s: []	p: 0	w: 1
 ||       u11	s: []	p: 2	w: max(x3 + 3, x4 + 4)
 ||       sel	s: []	p: 3	w: x2 + 8
 ||       afterNth	s: []	p: 0	w: x2 + 6
 ||       nil	s: []	p: 2	w: 2
 ||       #axxsnd	s: []	p: 0	w: 1
 ||       #TIlDePAIR	s: [1]	p: 0	w: x1
 ||       axxafterNth	s: []	p: 0	w: x2 + 6
 ||       mark	s: 1
 ||       u12	s: [2]	p: 1	w: max(x1, x2 + 2)
 ||       axxsel	s: []	p: 3	w: x2 + 8
 ||       axxfst	s: []	p: 3	w: x1 + 1
 ||       #axxand	s: []	p: 0	w: x2 + 1
 ||       #axxsel	s: []	p: 0	w: 1
 ||       head	s: [1]	p: 0	w: x1 + 1
 ||       cons	s: [1]	p: 4	w: max(x1 + 1, x2)
 ||       snd	s: []	p: 0	w: x1 + 1
 ||       axxu12	s: [2]	p: 1	w: max(x1, x2 + 2)
 ||       axxtail	s: [1]	p: 3	w: x1 + 1
 ||       tt	s: []	p: 2	w: 0
 ||       axxtake	s: []	p: 4	w: x2 + 6
 ||       #axxfst	s: []	p: 0	w: 0
 ||       #axxtake	s: []	p: 0	w: x2 + 1
 ||       #axxhead	s: []	p: 0	w: 0
 ||       axxhead	s: [1]	p: 0	w: x1 + 1
 ||     USABLE RULES: { 1..43 }
 ||     Removed DPs: #10 #47
 || Number of SCCs: 0, DPs: 0
 || 
We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [FuhKop19]).

We thus obtain the following dependency pair problem (P_0, R_0, computable, formative):

  Dependency Pairs P_0:

    0] foldr#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> foldr#(/\z./\u.X(z, u), Y, U) {X : 2}  

  Rules R_0:

    axxu11(tt, X, Y, Z) => axxu12(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu12(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxafterNth(X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxand(tt, X) => mark(X) 
    axxfst(pair(X, Y)) => mark(X) 
    axxhead(cons(X, Y)) => mark(X) 
    axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
    axxsel(X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxsnd(pair(X, Y)) => mark(Y) 
    axxsplitAt(0, X) => pair(nil, mark(X)) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu11(tt, X, Y, Z) 
    axxtail(cons(X, Y)) => mark(Y) 
    axxtake(X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    mark(u11(X, Y, Z, U)) => axxu11(mark(X), Y, Z, U) 
    mark(u12(X, Y)) => axxu12(mark(X), Y) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(and(X, Y)) => axxand(mark(X), Y) 
    mark(fst(X)) => axxfst(mark(X)) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
    mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
    mark(tail(X)) => axxtail(mark(X)) 
    mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
    mark(tt) => tt 
    mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
    mark(cons(X, Y)) => cons(mark(X), Y) 
    mark(s(X)) => s(mark(X)) 
    mark(0) => 0 
    mark(nil) => nil 
    axxu11(X, Y, Z, U) => u11(X, Y, Z, U) 
    axxu12(X, Y) => u12(X, Y) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxsnd(X) => snd(X) 
    axxand(X, Y) => and(X, Y) 
    axxfst(X) => fst(X) 
    axxhead(X) => head(X) 
    axxnatsFrom(X) => natsFrom(X) 
    axxsel(X, Y) => sel(X, Y) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    foldr(/\x./\y.X(x, y), Y, nil) => Y 
    foldr(/\x./\y.X(x, y), Y, cons(Z, U)) => X(Z, foldr(/\z./\u.X(z, u), Y, U)) 

Thus, the original system is terminating if (P_0, R_0, computable, formative) is finite.

We consider the dependency pair problem (P_0, R_0, computable, formative).

We apply the subterm criterion with the following projection function:

  nu(foldr#) = 3 

Thus, we can orient the dependency pairs as follows:

  nu(foldr#(/\x./\y.X(x, y), Y, cons(Z, U))) = cons(Z, U) |> U = nu(foldr#(/\z./\u.X(z, u), Y, U)) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_0, R_0, computable, f) by ({}, R_0, computable, f).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[FuhKop19]  C. Fuhs, and C. Kop.  A static higher-order dependency pair framework.  In Proceedings of ESOP 2019, 2019.
[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.
[KusIsoSakBla09]  K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui.  Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems.  In volume 92(10) of IEICE Transactions on Information and Systems.  2007--2015, 2009.