We consider the system h40.

  Alphabet:

    0 : [] --> A 
    afterNth : [] --> A -> A -> A 
    app : [] --> (A -> A) -> A -> A 
    axxafterNth : [] --> 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 
    axxu12 : [] --> A -> A -> A -> A 
    axxu21 : [] --> A -> A -> A 
    axxu22 : [] --> A -> A -> A 
    axxu31 : [] --> A -> A -> A 
    axxu32 : [] --> A -> A -> A 
    axxu41 : [] --> A -> A -> A -> A 
    axxu42 : [] --> A -> A -> A -> A 
    axxu51 : [] --> A -> A -> A 
    axxu52 : [] --> A -> A -> A 
    axxu61 : [] --> A -> A -> A -> A -> A 
    axxu62 : [] --> A -> A -> A -> A -> A 
    axxu63 : [] --> A -> A -> A -> A -> A 
    axxu64 : [] --> A -> A -> A 
    axxu71 : [] --> A -> A -> A 
    axxu72 : [] --> A -> A -> A 
    axxu81 : [] --> A -> A -> A -> A 
    axxu82 : [] --> A -> A -> A -> A 
    cons : [] --> A -> A -> A 
    fst : [] --> A -> A 
    head : [] --> A -> A 
    map : [] --> (A -> A) -> 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 
    u12 : [] --> A -> A -> A -> A 
    u21 : [] --> A -> A -> A 
    u22 : [] --> A -> A -> A 
    u31 : [] --> A -> A -> A 
    u32 : [] --> A -> A -> A 
    u41 : [] --> A -> A -> A -> A 
    u42 : [] --> A -> A -> A -> A 
    u51 : [] --> A -> A -> A 
    u52 : [] --> A -> A -> A 
    u61 : [] --> A -> A -> A -> A -> A 
    u62 : [] --> A -> A -> A -> A -> A 
    u63 : [] --> A -> A -> A -> A -> A 
    u64 : [] --> A -> A -> A 
    u71 : [] --> A -> A -> A 
    u72 : [] --> A -> A -> A 
    u81 : [] --> A -> A -> A -> A 
    u82 : [] --> A -> A -> A -> A 

  Rules:

    axxu11 tt x y => axxu12 tt x y 
    axxu12 tt x y => axxsnd (axxsplitAt (mark x) (mark y)) 
    axxu21 tt x => axxu22 tt x 
    axxu22 tt x => mark x 
    axxu31 tt x => axxu32 tt x 
    axxu32 tt x => mark x 
    axxu41 tt x y => axxu42 tt x y 
    axxu42 tt x y => axxhead (axxafterNth (mark x) (mark y)) 
    axxu51 tt x => axxu52 tt x 
    axxu52 tt x => mark x 
    axxu61 tt x y z => axxu62 tt x y z 
    axxu62 tt x y z => axxu63 tt x y z 
    axxu63 tt x y z => axxu64 (axxsplitAt (mark x) (mark z)) y 
    axxu64 (pair x y) z => pair (cons (mark z) x) (mark y) 
    axxu71 tt x => axxu72 tt x 
    axxu72 tt x => mark x 
    axxu81 tt x y => axxu82 tt x y 
    axxu82 tt x y => axxfst (axxsplitAt (mark x) (mark y)) 
    axxafterNth x y => axxu11 tt x y 
    axxfst (pair x y) => axxu21 tt x 
    axxhead (cons x y) => axxu31 tt x 
    axxnatsFrom x => cons (mark x) (natsFrom (s x)) 
    axxsel x y => axxu41 tt x y 
    axxsnd (pair x y) => axxu51 tt y 
    axxsplitAt 0 x => pair nil (mark x) 
    axxsplitAt (s x) (cons y z) => axxu61 tt x y z 
    axxtail (cons x y) => axxu71 tt y 
    axxtake x y => axxu81 tt x y 
    mark (u11 x y z) => axxu11 (mark x) y z 
    mark (u12 x y z) => axxu12 (mark x) y z 
    mark (snd x) => axxsnd (mark x) 
    mark (splitAt x y) => axxsplitAt (mark x) (mark y) 
    mark (u21 x y) => axxu21 (mark x) y 
    mark (u22 x y) => axxu22 (mark x) y 
    mark (u31 x y) => axxu31 (mark x) y 
    mark (u32 x y) => axxu32 (mark x) y 
    mark (u41 x y z) => axxu41 (mark x) y z 
    mark (u42 x y z) => axxu42 (mark x) y z 
    mark (head x) => axxhead (mark x) 
    mark (afterNth x y) => axxafterNth (mark x) (mark y) 
    mark (u51 x y) => axxu51 (mark x) y 
    mark (u52 x y) => axxu52 (mark x) y 
    mark (u61 x y z u) => axxu61 (mark x) y z u 
    mark (u62 x y z u) => axxu62 (mark x) y z u 
    mark (u63 x y z u) => axxu63 (mark x) y z u 
    mark (u64 x y) => axxu64 (mark x) y 
    mark (u71 x y) => axxu71 (mark x) y 
    mark (u72 x y) => axxu72 (mark x) y 
    mark (u81 x y z) => axxu81 (mark x) y z 
    mark (u82 x y z) => axxu82 (mark x) y z 
    mark (fst x) => axxfst (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 => u11 x y z 
    axxu12 x y z => u12 x y z 
    axxsnd x => snd x 
    axxsplitAt x y => splitAt x y 
    axxu21 x y => u21 x y 
    axxu22 x y => u22 x y 
    axxu31 x y => u31 x y 
    axxu32 x y => u32 x y 
    axxu41 x y z => u41 x y z 
    axxu42 x y z => u42 x y z 
    axxhead x => head x 
    axxafterNth x y => afterNth x y 
    axxu51 x y => u51 x y 
    axxu52 x y => u52 x y 
    axxu61 x y z u => u61 x y z u 
    axxu62 x y z u => u62 x y z u 
    axxu63 x y z u => u63 x y z u 
    axxu64 x y => u64 x y 
    axxu71 x y => u71 x y 
    axxu72 x y => u72 x y 
    axxu81 x y z => u81 x y z 
    axxu82 x y z => u82 x y z 
    axxfst x => fst x 
    axxnatsFrom x => natsFrom x 
    axxsel x y => sel x y 
    axxtail x => tail x 
    axxtake x y => take x y 
    map (/\x.f x) nil => nil 
    map (/\x.f x) (cons y z) => cons (f y) (map (/\u.f u) z) 
    app (/\x.f x) y => f y 

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 
    app : [A -> A * A] --> A 
    axxafterNth : [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 
    axxu12 : [A * A * A] --> A 
    axxu21 : [A * A] --> A 
    axxu22 : [A * A] --> A 
    axxu31 : [A * A] --> A 
    axxu32 : [A * A] --> A 
    axxu41 : [A * A * A] --> A 
    axxu42 : [A * A * A] --> A 
    axxu51 : [A * A] --> A 
    axxu52 : [A * A] --> A 
    axxu61 : [A * A * A * A] --> A 
    axxu62 : [A * A * A * A] --> A 
    axxu63 : [A * A * A * A] --> A 
    axxu64 : [A * A] --> A 
    axxu71 : [A * A] --> A 
    axxu72 : [A * A] --> A 
    axxu81 : [A * A * A] --> A 
    axxu82 : [A * A * A] --> A 
    cons : [A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    map : [A -> A * 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 
    u12 : [A * A * A] --> A 
    u21 : [A * A] --> A 
    u22 : [A * A] --> A 
    u31 : [A * A] --> A 
    u32 : [A * A] --> A 
    u41 : [A * A * A] --> A 
    u42 : [A * A * A] --> A 
    u51 : [A * A] --> A 
    u52 : [A * A] --> A 
    u61 : [A * A * A * A] --> A 
    u62 : [A * A * A * A] --> A 
    u63 : [A * A * A * A] --> A 
    u64 : [A * A] --> A 
    u71 : [A * A] --> A 
    u72 : [A * A] --> A 
    u81 : [A * A * A] --> A 
    u82 : [A * A * A] --> A 
    ~AP1 : [A -> A * A] --> A 

  Rules:

    axxu11(tt, X, Y) => axxu12(tt, X, Y) 
    axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxu21(tt, X) => axxu22(tt, X) 
    axxu22(tt, X) => mark(X) 
    axxu31(tt, X) => axxu32(tt, X) 
    axxu32(tt, X) => mark(X) 
    axxu41(tt, X, Y) => axxu42(tt, X, Y) 
    axxu42(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxu51(tt, X) => axxu52(tt, X) 
    axxu52(tt, X) => mark(X) 
    axxu61(tt, X, Y, Z) => axxu62(tt, X, Y, Z) 
    axxu62(tt, X, Y, Z) => axxu63(tt, X, Y, Z) 
    axxu63(tt, X, Y, Z) => axxu64(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu64(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxu71(tt, X) => axxu72(tt, X) 
    axxu72(tt, X) => mark(X) 
    axxu81(tt, X, Y) => axxu82(tt, X, Y) 
    axxu82(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    axxafterNth(X, Y) => axxu11(tt, X, Y) 
    axxfst(pair(X, Y)) => axxu21(tt, X) 
    axxhead(cons(X, Y)) => axxu31(tt, X) 
    axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
    axxsel(X, Y) => axxu41(tt, X, Y) 
    axxsnd(pair(X, Y)) => axxu51(tt, Y) 
    axxsplitAt(0, X) => pair(nil, mark(X)) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu61(tt, X, Y, Z) 
    axxtail(cons(X, Y)) => axxu71(tt, Y) 
    axxtake(X, Y) => axxu81(tt, X, Y) 
    mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
    mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(u21(X, Y)) => axxu21(mark(X), Y) 
    mark(u22(X, Y)) => axxu22(mark(X), Y) 
    mark(u31(X, Y)) => axxu31(mark(X), Y) 
    mark(u32(X, Y)) => axxu32(mark(X), Y) 
    mark(u41(X, Y, Z)) => axxu41(mark(X), Y, Z) 
    mark(u42(X, Y, Z)) => axxu42(mark(X), Y, Z) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(u51(X, Y)) => axxu51(mark(X), Y) 
    mark(u52(X, Y)) => axxu52(mark(X), Y) 
    mark(u61(X, Y, Z, U)) => axxu61(mark(X), Y, Z, U) 
    mark(u62(X, Y, Z, U)) => axxu62(mark(X), Y, Z, U) 
    mark(u63(X, Y, Z, U)) => axxu63(mark(X), Y, Z, U) 
    mark(u64(X, Y)) => axxu64(mark(X), Y) 
    mark(u71(X, Y)) => axxu71(mark(X), Y) 
    mark(u72(X, Y)) => axxu72(mark(X), Y) 
    mark(u81(X, Y, Z)) => axxu81(mark(X), Y, Z) 
    mark(u82(X, Y, Z)) => axxu82(mark(X), Y, Z) 
    mark(fst(X)) => axxfst(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) => u11(X, Y, Z) 
    axxu12(X, Y, Z) => u12(X, Y, Z) 
    axxsnd(X) => snd(X) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxu21(X, Y) => u21(X, Y) 
    axxu22(X, Y) => u22(X, Y) 
    axxu31(X, Y) => u31(X, Y) 
    axxu32(X, Y) => u32(X, Y) 
    axxu41(X, Y, Z) => u41(X, Y, Z) 
    axxu42(X, Y, Z) => u42(X, Y, Z) 
    axxhead(X) => head(X) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxu51(X, Y) => u51(X, Y) 
    axxu52(X, Y) => u52(X, Y) 
    axxu61(X, Y, Z, U) => u61(X, Y, Z, U) 
    axxu62(X, Y, Z, U) => u62(X, Y, Z, U) 
    axxu63(X, Y, Z, U) => u63(X, Y, Z, U) 
    axxu64(X, Y) => u64(X, Y) 
    axxu71(X, Y) => u71(X, Y) 
    axxu72(X, Y) => u72(X, Y) 
    axxu81(X, Y, Z) => u81(X, Y, Z) 
    axxu82(X, Y, Z) => u82(X, Y, Z) 
    axxfst(X) => fst(X) 
    axxnatsFrom(X) => natsFrom(X) 
    axxsel(X, Y) => sel(X, Y) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    map(/\x.~AP1(F, x), nil) => nil 
    map(/\x.~AP1(F, x), cons(X, Y)) => cons(~AP1(F, X), map(/\y.~AP1(F, y), Y)) 
    app(/\x.~AP1(F, x), X) => ~AP1(F, X) 
    map(/\x.afterNth(X, x), nil) => nil 
    map(/\x.app(F, x), nil) => nil 
    map(/\x.axxafterNth(X, x), nil) => nil 
    map(/\x.axxfst(x), nil) => nil 
    map(/\x.axxhead(x), nil) => nil 
    map(/\x.axxnatsFrom(x), nil) => nil 
    map(/\x.axxsel(X, x), nil) => nil 
    map(/\x.axxsnd(x), nil) => nil 
    map(/\x.axxsplitAt(X, x), nil) => nil 
    map(/\x.axxtail(x), nil) => nil 
    map(/\x.axxtake(X, x), nil) => nil 
    map(/\x.axxu11(X, Y, x), nil) => nil 
    map(/\x.axxu12(X, Y, x), nil) => nil 
    map(/\x.axxu21(X, x), nil) => nil 
    map(/\x.axxu22(X, x), nil) => nil 
    map(/\x.axxu31(X, x), nil) => nil 
    map(/\x.axxu32(X, x), nil) => nil 
    map(/\x.axxu41(X, Y, x), nil) => nil 
    map(/\x.axxu42(X, Y, x), nil) => nil 
    map(/\x.axxu51(X, x), nil) => nil 
    map(/\x.axxu52(X, x), nil) => nil 
    map(/\x.axxu61(X, Y, Z, x), nil) => nil 
    map(/\x.axxu62(X, Y, Z, x), nil) => nil 
    map(/\x.axxu63(X, Y, Z, x), nil) => nil 
    map(/\x.axxu64(X, x), nil) => nil 
    map(/\x.axxu71(X, x), nil) => nil 
    map(/\x.axxu72(X, x), nil) => nil 
    map(/\x.axxu81(X, Y, x), nil) => nil 
    map(/\x.axxu82(X, Y, x), nil) => nil 
    map(/\x.cons(X, x), nil) => nil 
    map(/\x.fst(x), nil) => nil 
    map(/\x.head(x), nil) => nil 
    map(/\x.map(F, x), nil) => nil 
    map(/\x.mark(x), nil) => nil 
    map(/\x.natsFrom(x), nil) => nil 
    map(/\x.pair(X, x), nil) => nil 
    map(/\x.s(x), nil) => nil 
    map(/\x.sel(X, x), nil) => nil 
    map(/\x.snd(x), nil) => nil 
    map(/\x.splitAt(X, x), nil) => nil 
    map(/\x.tail(x), nil) => nil 
    map(/\x.take(X, x), nil) => nil 
    map(/\x.u11(X, Y, x), nil) => nil 
    map(/\x.u12(X, Y, x), nil) => nil 
    map(/\x.u21(X, x), nil) => nil 
    map(/\x.u22(X, x), nil) => nil 
    map(/\x.u31(X, x), nil) => nil 
    map(/\x.u32(X, x), nil) => nil 
    map(/\x.u41(X, Y, x), nil) => nil 
    map(/\x.u42(X, Y, x), nil) => nil 
    map(/\x.u51(X, x), nil) => nil 
    map(/\x.u52(X, x), nil) => nil 
    map(/\x.u61(X, Y, Z, x), nil) => nil 
    map(/\x.u62(X, Y, Z, x), nil) => nil 
    map(/\x.u63(X, Y, Z, x), nil) => nil 
    map(/\x.u64(X, x), nil) => nil 
    map(/\x.u71(X, x), nil) => nil 
    map(/\x.u72(X, x), nil) => nil 
    map(/\x.u81(X, Y, x), nil) => nil 
    map(/\x.u82(X, Y, x), nil) => nil 
    map(/\x.afterNth(X, x), cons(Y, Z)) => cons(afterNth(X, Y), map(/\y.afterNth(X, y), Z)) 
    map(/\x.app(F, x), cons(X, Y)) => cons(app(F, X), map(/\y.app(F, y), Y)) 
    map(/\x.axxafterNth(X, x), cons(Y, Z)) => cons(axxafterNth(X, Y), map(/\y.axxafterNth(X, y), Z)) 
    map(/\x.axxfst(x), cons(X, Y)) => cons(axxfst(X), map(/\y.axxfst(y), Y)) 
    map(/\x.axxhead(x), cons(X, Y)) => cons(axxhead(X), map(/\y.axxhead(y), Y)) 
    map(/\x.axxnatsFrom(x), cons(X, Y)) => cons(axxnatsFrom(X), map(/\y.axxnatsFrom(y), Y)) 
    map(/\x.axxsel(X, x), cons(Y, Z)) => cons(axxsel(X, Y), map(/\y.axxsel(X, y), Z)) 
    map(/\x.axxsnd(x), cons(X, Y)) => cons(axxsnd(X), map(/\y.axxsnd(y), Y)) 
    map(/\x.axxsplitAt(X, x), cons(Y, Z)) => cons(axxsplitAt(X, Y), map(/\y.axxsplitAt(X, y), Z)) 
    map(/\x.axxtail(x), cons(X, Y)) => cons(axxtail(X), map(/\y.axxtail(y), Y)) 
    map(/\x.axxtake(X, x), cons(Y, Z)) => cons(axxtake(X, Y), map(/\y.axxtake(X, y), Z)) 
    map(/\x.axxu11(X, Y, x), cons(Z, U)) => cons(axxu11(X, Y, Z), map(/\y.axxu11(X, Y, y), U)) 
    map(/\x.axxu12(X, Y, x), cons(Z, U)) => cons(axxu12(X, Y, Z), map(/\y.axxu12(X, Y, y), U)) 
    map(/\x.axxu21(X, x), cons(Y, Z)) => cons(axxu21(X, Y), map(/\y.axxu21(X, y), Z)) 
    map(/\x.axxu22(X, x), cons(Y, Z)) => cons(axxu22(X, Y), map(/\y.axxu22(X, y), Z)) 
    map(/\x.axxu31(X, x), cons(Y, Z)) => cons(axxu31(X, Y), map(/\y.axxu31(X, y), Z)) 
    map(/\x.axxu32(X, x), cons(Y, Z)) => cons(axxu32(X, Y), map(/\y.axxu32(X, y), Z)) 
    map(/\x.axxu41(X, Y, x), cons(Z, U)) => cons(axxu41(X, Y, Z), map(/\y.axxu41(X, Y, y), U)) 
    map(/\x.axxu42(X, Y, x), cons(Z, U)) => cons(axxu42(X, Y, Z), map(/\y.axxu42(X, Y, y), U)) 
    map(/\x.axxu51(X, x), cons(Y, Z)) => cons(axxu51(X, Y), map(/\y.axxu51(X, y), Z)) 
    map(/\x.axxu52(X, x), cons(Y, Z)) => cons(axxu52(X, Y), map(/\y.axxu52(X, y), Z)) 
    map(/\x.axxu61(X, Y, Z, x), cons(U, V)) => cons(axxu61(X, Y, Z, U), map(/\y.axxu61(X, Y, Z, y), V)) 
    map(/\x.axxu62(X, Y, Z, x), cons(U, V)) => cons(axxu62(X, Y, Z, U), map(/\y.axxu62(X, Y, Z, y), V)) 
    map(/\x.axxu63(X, Y, Z, x), cons(U, V)) => cons(axxu63(X, Y, Z, U), map(/\y.axxu63(X, Y, Z, y), V)) 
    map(/\x.axxu64(X, x), cons(Y, Z)) => cons(axxu64(X, Y), map(/\y.axxu64(X, y), Z)) 
    map(/\x.axxu71(X, x), cons(Y, Z)) => cons(axxu71(X, Y), map(/\y.axxu71(X, y), Z)) 
    map(/\x.axxu72(X, x), cons(Y, Z)) => cons(axxu72(X, Y), map(/\y.axxu72(X, y), Z)) 
    map(/\x.axxu81(X, Y, x), cons(Z, U)) => cons(axxu81(X, Y, Z), map(/\y.axxu81(X, Y, y), U)) 
    map(/\x.axxu82(X, Y, x), cons(Z, U)) => cons(axxu82(X, Y, Z), map(/\y.axxu82(X, Y, y), U)) 
    map(/\x.cons(X, x), cons(Y, Z)) => cons(cons(X, Y), map(/\y.cons(X, y), Z)) 
    map(/\x.fst(x), cons(X, Y)) => cons(fst(X), map(/\y.fst(y), Y)) 
    map(/\x.head(x), cons(X, Y)) => cons(head(X), map(/\y.head(y), Y)) 
    map(/\x.map(F, x), cons(X, Y)) => cons(map(F, X), map(/\y.map(F, y), Y)) 
    map(/\x.mark(x), cons(X, Y)) => cons(mark(X), map(/\y.mark(y), Y)) 
    map(/\x.natsFrom(x), cons(X, Y)) => cons(natsFrom(X), map(/\y.natsFrom(y), Y)) 
    map(/\x.pair(X, x), cons(Y, Z)) => cons(pair(X, Y), map(/\y.pair(X, y), Z)) 
    map(/\x.s(x), cons(X, Y)) => cons(s(X), map(/\y.s(y), Y)) 
    map(/\x.sel(X, x), cons(Y, Z)) => cons(sel(X, Y), map(/\y.sel(X, y), Z)) 
    map(/\x.snd(x), cons(X, Y)) => cons(snd(X), map(/\y.snd(y), Y)) 
    map(/\x.splitAt(X, x), cons(Y, Z)) => cons(splitAt(X, Y), map(/\y.splitAt(X, y), Z)) 
    map(/\x.tail(x), cons(X, Y)) => cons(tail(X), map(/\y.tail(y), Y)) 
    map(/\x.take(X, x), cons(Y, Z)) => cons(take(X, Y), map(/\y.take(X, y), Z)) 
    map(/\x.u11(X, Y, x), cons(Z, U)) => cons(u11(X, Y, Z), map(/\y.u11(X, Y, y), U)) 
    map(/\x.u12(X, Y, x), cons(Z, U)) => cons(u12(X, Y, Z), map(/\y.u12(X, Y, y), U)) 
    map(/\x.u21(X, x), cons(Y, Z)) => cons(u21(X, Y), map(/\y.u21(X, y), Z)) 
    map(/\x.u22(X, x), cons(Y, Z)) => cons(u22(X, Y), map(/\y.u22(X, y), Z)) 
    map(/\x.u31(X, x), cons(Y, Z)) => cons(u31(X, Y), map(/\y.u31(X, y), Z)) 
    map(/\x.u32(X, x), cons(Y, Z)) => cons(u32(X, Y), map(/\y.u32(X, y), Z)) 
    map(/\x.u41(X, Y, x), cons(Z, U)) => cons(u41(X, Y, Z), map(/\y.u41(X, Y, y), U)) 
    map(/\x.u42(X, Y, x), cons(Z, U)) => cons(u42(X, Y, Z), map(/\y.u42(X, Y, y), U)) 
    map(/\x.u51(X, x), cons(Y, Z)) => cons(u51(X, Y), map(/\y.u51(X, y), Z)) 
    map(/\x.u52(X, x), cons(Y, Z)) => cons(u52(X, Y), map(/\y.u52(X, y), Z)) 
    map(/\x.u61(X, Y, Z, x), cons(U, V)) => cons(u61(X, Y, Z, U), map(/\y.u61(X, Y, Z, y), V)) 
    map(/\x.u62(X, Y, Z, x), cons(U, V)) => cons(u62(X, Y, Z, U), map(/\y.u62(X, Y, Z, y), V)) 
    map(/\x.u63(X, Y, Z, x), cons(U, V)) => cons(u63(X, Y, Z, U), map(/\y.u63(X, Y, Z, y), V)) 
    map(/\x.u64(X, x), cons(Y, Z)) => cons(u64(X, Y), map(/\y.u64(X, y), Z)) 
    map(/\x.u71(X, x), cons(Y, Z)) => cons(u71(X, Y), map(/\y.u71(X, y), Z)) 
    map(/\x.u72(X, x), cons(Y, Z)) => cons(u72(X, Y), map(/\y.u72(X, y), Z)) 
    map(/\x.u81(X, Y, x), cons(Z, U)) => cons(u81(X, Y, Z), map(/\y.u81(X, Y, y), U)) 
    map(/\x.u82(X, Y, x), cons(Z, U)) => cons(u82(X, Y, Z), map(/\y.u82(X, Y, y), U)) 
    app(/\x.afterNth(X, x), Y) => afterNth(X, Y) 
    app(/\x.app(F, x), X) => app(F, X) 
    app(/\x.axxafterNth(X, x), Y) => axxafterNth(X, Y) 
    app(/\x.axxfst(x), X) => axxfst(X) 
    app(/\x.axxhead(x), X) => axxhead(X) 
    app(/\x.axxnatsFrom(x), X) => axxnatsFrom(X) 
    app(/\x.axxsel(X, x), Y) => axxsel(X, Y) 
    app(/\x.axxsnd(x), X) => axxsnd(X) 
    app(/\x.axxsplitAt(X, x), Y) => axxsplitAt(X, Y) 
    app(/\x.axxtail(x), X) => axxtail(X) 
    app(/\x.axxtake(X, x), Y) => axxtake(X, Y) 
    app(/\x.axxu11(X, Y, x), Z) => axxu11(X, Y, Z) 
    app(/\x.axxu12(X, Y, x), Z) => axxu12(X, Y, Z) 
    app(/\x.axxu21(X, x), Y) => axxu21(X, Y) 
    app(/\x.axxu22(X, x), Y) => axxu22(X, Y) 
    app(/\x.axxu31(X, x), Y) => axxu31(X, Y) 
    app(/\x.axxu32(X, x), Y) => axxu32(X, Y) 
    app(/\x.axxu41(X, Y, x), Z) => axxu41(X, Y, Z) 
    app(/\x.axxu42(X, Y, x), Z) => axxu42(X, Y, Z) 
    app(/\x.axxu51(X, x), Y) => axxu51(X, Y) 
    app(/\x.axxu52(X, x), Y) => axxu52(X, Y) 
    app(/\x.axxu61(X, Y, Z, x), U) => axxu61(X, Y, Z, U) 
    app(/\x.axxu62(X, Y, Z, x), U) => axxu62(X, Y, Z, U) 
    app(/\x.axxu63(X, Y, Z, x), U) => axxu63(X, Y, Z, U) 
    app(/\x.axxu64(X, x), Y) => axxu64(X, Y) 
    app(/\x.axxu71(X, x), Y) => axxu71(X, Y) 
    app(/\x.axxu72(X, x), Y) => axxu72(X, Y) 
    app(/\x.axxu81(X, Y, x), Z) => axxu81(X, Y, Z) 
    app(/\x.axxu82(X, Y, x), Z) => axxu82(X, Y, Z) 
    app(/\x.cons(X, x), Y) => cons(X, Y) 
    app(/\x.fst(x), X) => fst(X) 
    app(/\x.head(x), X) => head(X) 
    app(/\x.map(F, x), X) => map(F, X) 
    app(/\x.mark(x), X) => mark(X) 
    app(/\x.natsFrom(x), X) => natsFrom(X) 
    app(/\x.pair(X, x), Y) => pair(X, Y) 
    app(/\x.s(x), X) => s(X) 
    app(/\x.sel(X, x), Y) => sel(X, Y) 
    app(/\x.snd(x), X) => snd(X) 
    app(/\x.splitAt(X, x), Y) => splitAt(X, Y) 
    app(/\x.tail(x), X) => tail(X) 
    app(/\x.take(X, x), Y) => take(X, Y) 
    app(/\x.u11(X, Y, x), Z) => u11(X, Y, Z) 
    app(/\x.u12(X, Y, x), Z) => u12(X, Y, Z) 
    app(/\x.u21(X, x), Y) => u21(X, Y) 
    app(/\x.u22(X, x), Y) => u22(X, Y) 
    app(/\x.u31(X, x), Y) => u31(X, Y) 
    app(/\x.u32(X, x), Y) => u32(X, Y) 
    app(/\x.u41(X, Y, x), Z) => u41(X, Y, Z) 
    app(/\x.u42(X, Y, x), Z) => u42(X, Y, Z) 
    app(/\x.u51(X, x), Y) => u51(X, Y) 
    app(/\x.u52(X, x), Y) => u52(X, Y) 
    app(/\x.u61(X, Y, Z, x), U) => u61(X, Y, Z, U) 
    app(/\x.u62(X, Y, Z, x), U) => u62(X, Y, Z, U) 
    app(/\x.u63(X, Y, Z, x), U) => u63(X, Y, Z, U) 
    app(/\x.u64(X, x), Y) => u64(X, Y) 
    app(/\x.u71(X, x), Y) => u71(X, Y) 
    app(/\x.u72(X, x), Y) => u72(X, Y) 
    app(/\x.u81(X, Y, x), Z) => u81(X, Y, Z) 
    app(/\x.u82(X, Y, x), Z) => u82(X, Y, 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 
    app : [A -> A * A] --> A 
    axxafterNth : [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 
    axxu12 : [A * A * A] --> A 
    axxu21 : [A * A] --> A 
    axxu22 : [A * A] --> A 
    axxu31 : [A * A] --> A 
    axxu32 : [A * A] --> A 
    axxu41 : [A * A * A] --> A 
    axxu42 : [A * A * A] --> A 
    axxu51 : [A * A] --> A 
    axxu52 : [A * A] --> A 
    axxu61 : [A * A * A * A] --> A 
    axxu62 : [A * A * A * A] --> A 
    axxu63 : [A * A * A * A] --> A 
    axxu64 : [A * A] --> A 
    axxu71 : [A * A] --> A 
    axxu72 : [A * A] --> A 
    axxu81 : [A * A * A] --> A 
    axxu82 : [A * A * A] --> A 
    cons : [A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    map : [A -> A * 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 
    u12 : [A * A * A] --> A 
    u21 : [A * A] --> A 
    u22 : [A * A] --> A 
    u31 : [A * A] --> A 
    u32 : [A * A] --> A 
    u41 : [A * A * A] --> A 
    u42 : [A * A * A] --> A 
    u51 : [A * A] --> A 
    u52 : [A * A] --> A 
    u61 : [A * A * A * A] --> A 
    u62 : [A * A * A * A] --> A 
    u63 : [A * A * A * A] --> A 
    u64 : [A * A] --> A 
    u71 : [A * A] --> A 
    u72 : [A * A] --> A 
    u81 : [A * A * A] --> A 
    u82 : [A * A * A] --> A 

  Rules:

    axxu11(tt, X, Y) => axxu12(tt, X, Y) 
    axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxu21(tt, X) => axxu22(tt, X) 
    axxu22(tt, X) => mark(X) 
    axxu31(tt, X) => axxu32(tt, X) 
    axxu32(tt, X) => mark(X) 
    axxu41(tt, X, Y) => axxu42(tt, X, Y) 
    axxu42(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxu51(tt, X) => axxu52(tt, X) 
    axxu52(tt, X) => mark(X) 
    axxu61(tt, X, Y, Z) => axxu62(tt, X, Y, Z) 
    axxu62(tt, X, Y, Z) => axxu63(tt, X, Y, Z) 
    axxu63(tt, X, Y, Z) => axxu64(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu64(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxu71(tt, X) => axxu72(tt, X) 
    axxu72(tt, X) => mark(X) 
    axxu81(tt, X, Y) => axxu82(tt, X, Y) 
    axxu82(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    axxafterNth(X, Y) => axxu11(tt, X, Y) 
    axxfst(pair(X, Y)) => axxu21(tt, X) 
    axxhead(cons(X, Y)) => axxu31(tt, X) 
    axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
    axxsel(X, Y) => axxu41(tt, X, Y) 
    axxsnd(pair(X, Y)) => axxu51(tt, Y) 
    axxsplitAt(0, X) => pair(nil, mark(X)) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu61(tt, X, Y, Z) 
    axxtail(cons(X, Y)) => axxu71(tt, Y) 
    axxtake(X, Y) => axxu81(tt, X, Y) 
    mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
    mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(u21(X, Y)) => axxu21(mark(X), Y) 
    mark(u22(X, Y)) => axxu22(mark(X), Y) 
    mark(u31(X, Y)) => axxu31(mark(X), Y) 
    mark(u32(X, Y)) => axxu32(mark(X), Y) 
    mark(u41(X, Y, Z)) => axxu41(mark(X), Y, Z) 
    mark(u42(X, Y, Z)) => axxu42(mark(X), Y, Z) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(u51(X, Y)) => axxu51(mark(X), Y) 
    mark(u52(X, Y)) => axxu52(mark(X), Y) 
    mark(u61(X, Y, Z, U)) => axxu61(mark(X), Y, Z, U) 
    mark(u62(X, Y, Z, U)) => axxu62(mark(X), Y, Z, U) 
    mark(u63(X, Y, Z, U)) => axxu63(mark(X), Y, Z, U) 
    mark(u64(X, Y)) => axxu64(mark(X), Y) 
    mark(u71(X, Y)) => axxu71(mark(X), Y) 
    mark(u72(X, Y)) => axxu72(mark(X), Y) 
    mark(u81(X, Y, Z)) => axxu81(mark(X), Y, Z) 
    mark(u82(X, Y, Z)) => axxu82(mark(X), Y, Z) 
    mark(fst(X)) => axxfst(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) => u11(X, Y, Z) 
    axxu12(X, Y, Z) => u12(X, Y, Z) 
    axxsnd(X) => snd(X) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxu21(X, Y) => u21(X, Y) 
    axxu22(X, Y) => u22(X, Y) 
    axxu31(X, Y) => u31(X, Y) 
    axxu32(X, Y) => u32(X, Y) 
    axxu41(X, Y, Z) => u41(X, Y, Z) 
    axxu42(X, Y, Z) => u42(X, Y, Z) 
    axxhead(X) => head(X) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxu51(X, Y) => u51(X, Y) 
    axxu52(X, Y) => u52(X, Y) 
    axxu61(X, Y, Z, U) => u61(X, Y, Z, U) 
    axxu62(X, Y, Z, U) => u62(X, Y, Z, U) 
    axxu63(X, Y, Z, U) => u63(X, Y, Z, U) 
    axxu64(X, Y) => u64(X, Y) 
    axxu71(X, Y) => u71(X, Y) 
    axxu72(X, Y) => u72(X, Y) 
    axxu81(X, Y, Z) => u81(X, Y, Z) 
    axxu82(X, Y, Z) => u82(X, Y, Z) 
    axxfst(X) => fst(X) 
    axxnatsFrom(X) => natsFrom(X) 
    axxsel(X, Y) => sel(X, Y) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    map(/\x.X(x), nil) => nil 
    map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    app(/\x.X(x), Y) => X(Y) 

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

  axxu11(tt, X, Y) => axxu12(tt, X, Y) 
  axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
  axxu21(tt, X) => axxu22(tt, X) 
  axxu22(tt, X) => mark(X) 
  axxu31(tt, X) => axxu32(tt, X) 
  axxu32(tt, X) => mark(X) 
  axxu41(tt, X, Y) => axxu42(tt, X, Y) 
  axxu42(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
  axxu51(tt, X) => axxu52(tt, X) 
  axxu52(tt, X) => mark(X) 
  axxu61(tt, X, Y, Z) => axxu62(tt, X, Y, Z) 
  axxu62(tt, X, Y, Z) => axxu63(tt, X, Y, Z) 
  axxu63(tt, X, Y, Z) => axxu64(axxsplitAt(mark(X), mark(Z)), Y) 
  axxu64(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
  axxu71(tt, X) => axxu72(tt, X) 
  axxu72(tt, X) => mark(X) 
  axxu81(tt, X, Y) => axxu82(tt, X, Y) 
  axxu82(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
  axxafterNth(X, Y) => axxu11(tt, X, Y) 
  axxfst(pair(X, Y)) => axxu21(tt, X) 
  axxhead(cons(X, Y)) => axxu31(tt, X) 
  axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
  axxsel(X, Y) => axxu41(tt, X, Y) 
  axxsnd(pair(X, Y)) => axxu51(tt, Y) 
  axxsplitAt(0, X) => pair(nil, mark(X)) 
  axxsplitAt(s(X), cons(Y, Z)) => axxu61(tt, X, Y, Z) 
  axxtail(cons(X, Y)) => axxu71(tt, Y) 
  axxtake(X, Y) => axxu81(tt, X, Y) 
  mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
  mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) 
  mark(snd(X)) => axxsnd(mark(X)) 
  mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
  mark(u21(X, Y)) => axxu21(mark(X), Y) 
  mark(u22(X, Y)) => axxu22(mark(X), Y) 
  mark(u31(X, Y)) => axxu31(mark(X), Y) 
  mark(u32(X, Y)) => axxu32(mark(X), Y) 
  mark(u41(X, Y, Z)) => axxu41(mark(X), Y, Z) 
  mark(u42(X, Y, Z)) => axxu42(mark(X), Y, Z) 
  mark(head(X)) => axxhead(mark(X)) 
  mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
  mark(u51(X, Y)) => axxu51(mark(X), Y) 
  mark(u52(X, Y)) => axxu52(mark(X), Y) 
  mark(u61(X, Y, Z, U)) => axxu61(mark(X), Y, Z, U) 
  mark(u62(X, Y, Z, U)) => axxu62(mark(X), Y, Z, U) 
  mark(u63(X, Y, Z, U)) => axxu63(mark(X), Y, Z, U) 
  mark(u64(X, Y)) => axxu64(mark(X), Y) 
  mark(u71(X, Y)) => axxu71(mark(X), Y) 
  mark(u72(X, Y)) => axxu72(mark(X), Y) 
  mark(u81(X, Y, Z)) => axxu81(mark(X), Y, Z) 
  mark(u82(X, Y, Z)) => axxu82(mark(X), Y, Z) 
  mark(fst(X)) => axxfst(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) => u11(X, Y, Z) 
  axxu12(X, Y, Z) => u12(X, Y, Z) 
  axxsnd(X) => snd(X) 
  axxsplitAt(X, Y) => splitAt(X, Y) 
  axxu21(X, Y) => u21(X, Y) 
  axxu22(X, Y) => u22(X, Y) 
  axxu31(X, Y) => u31(X, Y) 
  axxu32(X, Y) => u32(X, Y) 
  axxu41(X, Y, Z) => u41(X, Y, Z) 
  axxu42(X, Y, Z) => u42(X, Y, Z) 
  axxhead(X) => head(X) 
  axxafterNth(X, Y) => afterNth(X, Y) 
  axxu51(X, Y) => u51(X, Y) 
  axxu52(X, Y) => u52(X, Y) 
  axxu61(X, Y, Z, U) => u61(X, Y, Z, U) 
  axxu62(X, Y, Z, U) => u62(X, Y, Z, U) 
  axxu63(X, Y, Z, U) => u63(X, Y, Z, U) 
  axxu64(X, Y) => u64(X, Y) 
  axxu71(X, Y) => u71(X, Y) 
  axxu72(X, Y) => u72(X, Y) 
  axxu81(X, Y, Z) => u81(X, Y, Z) 
  axxu82(X, Y, Z) => u82(X, Y, Z) 
  axxfst(X) => fst(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) -> axxu12(tt(),PeRCenTX,PeRCenTY)
 ||     2: axxu12(tt(),PeRCenTX,PeRCenTY) -> axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     3: axxu21(tt(),PeRCenTX) -> axxu22(tt(),PeRCenTX)
 ||     4: axxu22(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     5: axxu31(tt(),PeRCenTX) -> axxu32(tt(),PeRCenTX)
 ||     6: axxu32(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     7: axxu41(tt(),PeRCenTX,PeRCenTY) -> axxu42(tt(),PeRCenTX,PeRCenTY)
 ||     8: axxu42(tt(),PeRCenTX,PeRCenTY) -> axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||     9: axxu51(tt(),PeRCenTX) -> axxu52(tt(),PeRCenTX)
 ||     10: axxu52(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     11: axxu61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     12: axxu62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     13: axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu64(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY)
 ||     14: axxu64(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> pair(cons(mark(PeRCenTZ),PeRCenTX),mark(PeRCenTY))
 ||     15: axxu71(tt(),PeRCenTX) -> axxu72(tt(),PeRCenTX)
 ||     16: axxu72(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     17: axxu81(tt(),PeRCenTX,PeRCenTY) -> axxu82(tt(),PeRCenTX,PeRCenTY)
 ||     18: axxu82(tt(),PeRCenTX,PeRCenTY) -> axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     19: axxafterNth(PeRCenTX,PeRCenTY) -> axxu11(tt(),PeRCenTX,PeRCenTY)
 ||     20: axxfst(pair(PeRCenTX,PeRCenTY)) -> axxu21(tt(),PeRCenTX)
 ||     21: axxhead(cons(PeRCenTX,PeRCenTY)) -> axxu31(tt(),PeRCenTX)
 ||     22: axxnatsFrom(PeRCenTX) -> cons(mark(PeRCenTX),natsFrom(s(PeRCenTX)))
 ||     23: axxsel(PeRCenTX,PeRCenTY) -> axxu41(tt(),PeRCenTX,PeRCenTY)
 ||     24: axxsnd(pair(PeRCenTX,PeRCenTY)) -> axxu51(tt(),PeRCenTY)
 ||     25: axxsplitAt(0(),PeRCenTX) -> pair(nil(),mark(PeRCenTX))
 ||     26: axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> axxu61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     27: axxtail(cons(PeRCenTX,PeRCenTY)) -> axxu71(tt(),PeRCenTY)
 ||     28: axxtake(PeRCenTX,PeRCenTY) -> axxu81(tt(),PeRCenTX,PeRCenTY)
 ||     29: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     30: mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu12(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     31: mark(snd(PeRCenTX)) -> axxsnd(mark(PeRCenTX))
 ||     32: mark(splitAt(PeRCenTX,PeRCenTY)) -> axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||     33: mark(u21(PeRCenTX,PeRCenTY)) -> axxu21(mark(PeRCenTX),PeRCenTY)
 ||     34: mark(u22(PeRCenTX,PeRCenTY)) -> axxu22(mark(PeRCenTX),PeRCenTY)
 ||     35: mark(u31(PeRCenTX,PeRCenTY)) -> axxu31(mark(PeRCenTX),PeRCenTY)
 ||     36: mark(u32(PeRCenTX,PeRCenTY)) -> axxu32(mark(PeRCenTX),PeRCenTY)
 ||     37: mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu41(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     38: mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu42(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     39: mark(head(PeRCenTX)) -> axxhead(mark(PeRCenTX))
 ||     40: mark(afterNth(PeRCenTX,PeRCenTY)) -> axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||     41: mark(u51(PeRCenTX,PeRCenTY)) -> axxu51(mark(PeRCenTX),PeRCenTY)
 ||     42: mark(u52(PeRCenTX,PeRCenTY)) -> axxu52(mark(PeRCenTX),PeRCenTY)
 ||     43: mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     44: mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     45: mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     46: mark(u64(PeRCenTX,PeRCenTY)) -> axxu64(mark(PeRCenTX),PeRCenTY)
 ||     47: mark(u71(PeRCenTX,PeRCenTY)) -> axxu71(mark(PeRCenTX),PeRCenTY)
 ||     48: mark(u72(PeRCenTX,PeRCenTY)) -> axxu72(mark(PeRCenTX),PeRCenTY)
 ||     49: mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu81(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     50: mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu82(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     51: mark(fst(PeRCenTX)) -> axxfst(mark(PeRCenTX))
 ||     52: mark(natsFrom(PeRCenTX)) -> axxnatsFrom(mark(PeRCenTX))
 ||     53: mark(sel(PeRCenTX,PeRCenTY)) -> axxsel(mark(PeRCenTX),mark(PeRCenTY))
 ||     54: mark(tail(PeRCenTX)) -> axxtail(mark(PeRCenTX))
 ||     55: mark(take(PeRCenTX,PeRCenTY)) -> axxtake(mark(PeRCenTX),mark(PeRCenTY))
 ||     56: mark(tt()) -> tt()
 ||     57: mark(pair(PeRCenTX,PeRCenTY)) -> pair(mark(PeRCenTX),mark(PeRCenTY))
 ||     58: mark(cons(PeRCenTX,PeRCenTY)) -> cons(mark(PeRCenTX),PeRCenTY)
 ||     59: mark(s(PeRCenTX)) -> s(mark(PeRCenTX))
 ||     60: mark(0()) -> 0()
 ||     61: mark(nil()) -> nil()
 ||     62: axxu11(PeRCenTX,PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     63: axxu12(PeRCenTX,PeRCenTY,PeRCenTZ) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     64: axxsnd(PeRCenTX) -> snd(PeRCenTX)
 ||     65: axxsplitAt(PeRCenTX,PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     66: axxu21(PeRCenTX,PeRCenTY) -> u21(PeRCenTX,PeRCenTY)
 ||     67: axxu22(PeRCenTX,PeRCenTY) -> u22(PeRCenTX,PeRCenTY)
 ||     68: axxu31(PeRCenTX,PeRCenTY) -> u31(PeRCenTX,PeRCenTY)
 ||     69: axxu32(PeRCenTX,PeRCenTY) -> u32(PeRCenTX,PeRCenTY)
 ||     70: axxu41(PeRCenTX,PeRCenTY,PeRCenTZ) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     71: axxu42(PeRCenTX,PeRCenTY,PeRCenTZ) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     72: axxhead(PeRCenTX) -> head(PeRCenTX)
 ||     73: axxafterNth(PeRCenTX,PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     74: axxu51(PeRCenTX,PeRCenTY) -> u51(PeRCenTX,PeRCenTY)
 ||     75: axxu52(PeRCenTX,PeRCenTY) -> u52(PeRCenTX,PeRCenTY)
 ||     76: axxu61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     77: axxu62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     78: axxu63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     79: axxu64(PeRCenTX,PeRCenTY) -> u64(PeRCenTX,PeRCenTY)
 ||     80: axxu71(PeRCenTX,PeRCenTY) -> u71(PeRCenTX,PeRCenTY)
 ||     81: axxu72(PeRCenTX,PeRCenTY) -> u72(PeRCenTX,PeRCenTY)
 ||     82: axxu81(PeRCenTX,PeRCenTY,PeRCenTZ) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     83: axxu82(PeRCenTX,PeRCenTY,PeRCenTZ) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     84: axxfst(PeRCenTX) -> fst(PeRCenTX)
 ||     85: axxnatsFrom(PeRCenTX) -> natsFrom(PeRCenTX)
 ||     86: axxsel(PeRCenTX,PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     87: axxtail(PeRCenTX) -> tail(PeRCenTX)
 ||     88: axxtake(PeRCenTX,PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     89: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX
 ||     90: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY
 || Number of strict rules: 90
 || Direct POLO(bPol) ... failed.
 || Uncurrying ... failed.
 || Dependency Pairs:
 ||    #1: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #2: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #3: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #4: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #5: #mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #6: #mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #7: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #8: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #9: #mark(u31(PeRCenTX,PeRCenTY)) -> #axxu31(mark(PeRCenTX),PeRCenTY)
 ||    #10: #mark(u31(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #11: #mark(u64(PeRCenTX,PeRCenTY)) -> #axxu64(mark(PeRCenTX),PeRCenTY)
 ||    #12: #mark(u64(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #13: #mark(u52(PeRCenTX,PeRCenTY)) -> #axxu52(mark(PeRCenTX),PeRCenTY)
 ||    #14: #mark(u52(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #15: #mark(u51(PeRCenTX,PeRCenTY)) -> #axxu51(mark(PeRCenTX),PeRCenTY)
 ||    #16: #mark(u51(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #17: #mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu41(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #18: #mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #19: #mark(u71(PeRCenTX,PeRCenTY)) -> #axxu71(mark(PeRCenTX),PeRCenTY)
 ||    #20: #mark(u71(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #21: #mark(sel(PeRCenTX,PeRCenTY)) -> #axxsel(mark(PeRCenTX),mark(PeRCenTY))
 ||    #22: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #23: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #24: #mark(u72(PeRCenTX,PeRCenTY)) -> #axxu72(mark(PeRCenTX),PeRCenTY)
 ||    #25: #mark(u72(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #26: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #27: #mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu42(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #28: #mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #29: #axxu32(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #30: #mark(s(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #31: #mark(take(PeRCenTX,PeRCenTY)) -> #axxtake(mark(PeRCenTX),mark(PeRCenTY))
 ||    #32: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #33: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #34: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #35: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #36: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #37: #mark(fst(PeRCenTX)) -> #axxfst(mark(PeRCenTX))
 ||    #38: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #39: #axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu64(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY)
 ||    #40: #axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ))
 ||    #41: #axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTX)
 ||    #42: #axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTZ)
 ||    #43: #axxu51(tt(),PeRCenTX) -> #axxu52(tt(),PeRCenTX)
 ||    #44: #axxu61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #45: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #46: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #47: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #axxu51(tt(),PeRCenTY)
 ||    #48: #axxsel(PeRCenTX,PeRCenTY) -> #axxu41(tt(),PeRCenTX,PeRCenTY)
 ||    #49: #mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #50: #mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #51: #axxu62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #52: #mark(snd(PeRCenTX)) -> #axxsnd(mark(PeRCenTX))
 ||    #53: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #54: #axxu64(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTZ)
 ||    #55: #axxu64(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTY)
 ||    #56: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu12(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #57: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #58: #mark(natsFrom(PeRCenTX)) -> #axxnatsFrom(mark(PeRCenTX))
 ||    #59: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #60: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu81(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #61: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #62: #axxsplitAt(0(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #63: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #axxu21(tt(),PeRCenTX)
 ||    #64: #axxu41(tt(),PeRCenTX,PeRCenTY) -> #axxu42(tt(),PeRCenTX,PeRCenTY)
 ||    #65: #mark(head(PeRCenTX)) -> #axxhead(mark(PeRCenTX))
 ||    #66: #mark(head(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #67: #axxu52(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #68: #mark(u21(PeRCenTX,PeRCenTY)) -> #axxu21(mark(PeRCenTX),PeRCenTY)
 ||    #69: #mark(u21(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #70: #axxu31(tt(),PeRCenTX) -> #axxu32(tt(),PeRCenTX)
 ||    #71: #mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #72: #mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #73: #axxtake(PeRCenTX,PeRCenTY) -> #axxu81(tt(),PeRCenTX,PeRCenTY)
 ||    #74: #axxnatsFrom(PeRCenTX) -> #mark(PeRCenTX)
 ||    #75: #mark(u22(PeRCenTX,PeRCenTY)) -> #axxu22(mark(PeRCenTX),PeRCenTY)
 ||    #76: #mark(u22(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #77: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #axxu71(tt(),PeRCenTY)
 ||    #78: #axxu81(tt(),PeRCenTX,PeRCenTY) -> #axxu82(tt(),PeRCenTX,PeRCenTY)
 ||    #79: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #80: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #81: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #82: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxu11(tt(),PeRCenTX,PeRCenTY)
 ||    #83: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxu61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #84: #mark(u32(PeRCenTX,PeRCenTY)) -> #axxu32(mark(PeRCenTX),PeRCenTY)
 ||    #85: #mark(u32(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #86: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #axxu31(tt(),PeRCenTX)
 ||    #87: #axxu72(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #88: #axxu21(tt(),PeRCenTX) -> #axxu22(tt(),PeRCenTX)
 ||    #89: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #axxu12(tt(),PeRCenTX,PeRCenTY)
 ||    #90: #mark(tail(PeRCenTX)) -> #axxtail(mark(PeRCenTX))
 ||    #91: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #92: #axxu42(tt(),PeRCenTX,PeRCenTY) -> #axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #93: #axxu42(tt(),PeRCenTX,PeRCenTY) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #94: #axxu42(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #95: #axxu42(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #96: #axxu71(tt(),PeRCenTX) -> #axxu72(tt(),PeRCenTX)
 ||    #97: #axxu22(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #98: #mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu82(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #99: #mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #100: #axxu82(tt(),PeRCenTX,PeRCenTY) -> #axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #101: #axxu82(tt(),PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #102: #axxu82(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #103: #axxu82(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 || Number of SCCs: 1, DPs: 103
 ||   SCC { #1..103 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1 + 19, x2 + 22, x3 + 18)
 ||       #axxu51	w: max(x1 + 16, x2 + 14)
 ||       #axxu32	w: max(x1 + 15, x2 + 13)
 ||       u62	w: max(x1 + 12, x2 + 16, x3 + 15, x4 + 17)
 ||       TIlDePAIR	w: 0
 ||       axxu62	w: max(x1 + 12, x2 + 16, x3 + 15, x4 + 17)
 ||       s 	w: x1
 ||       #axxu12	w: max(x1 + 31, x2 + 25, x3 + 25)
 ||       axxu63	w: max(x1 + 10, x2 + 16, x3 + 15, x4 + 17)
 ||       #axxu82	w: max(x2 + 21, x3 + 21)
 ||       axxsnd	w: x1 + 1
 ||       axxu11	w: max(x1 + 23, x2 + 29, x3 + 24)
 ||       axxu32	w: max(x1 + 8, x2 + 2)
 ||       take	w: max(x1 + 22, x2 + 23)
 ||       axxsplitAt	w: max(x1 + 16, x2 + 17)
 ||       pair	w: max(x1 + 12, x2 + 16)
 ||       fst	w: x1 + 1
 ||       natsFrom	w: x1 + 3
 ||       splitAt	w: max(x1 + 16, x2 + 17)
 ||       u52	w: max(x1 + 13, x2 + 14)
 ||       #axxu11	w: max(x2 + 34, x3 + 34)
 ||       axxu64	w: max(x1, x2 + 15)
 ||       u61	w: max(x1 + 18, x2 + 16, x3 + 15, x4 + 17)
 ||       axxu31	w: max(x1 + 7, x2 + 10)
 ||       #axxu64	w: max(x1 + 1, x2 + 13)
 ||       axxu72	w: max(x1 + 2, x2 + 3)
 ||       axxu22	w: max(x1 + 2, x2 + 3)
 ||       #axxsplitAt	w: max(x1 + 19, x2 + 20)
 ||       axxnatsFrom	w: x1 + 3
 ||       u41	w: max(x1 + 39, x2 + 42, x3 + 45)
 ||       u63	w: max(x1 + 10, x2 + 16, x3 + 15, x4 + 17)
 ||       u51	w: max(x1 + 15, x2 + 14)
 ||       tail	w: x1 + 4
 ||       #axxafterNth	w: max(x1 + 35, x2 + 35)
 ||       #mark	w: x1 + 12
 ||       #axxtail	w: x1 + 15
 ||       0 	w: 2
 ||       axxu82	w: max(x1 + 14, x2 + 22, x3 + 18)
 ||       #axxnatsFrom	w: x1 + 13
 ||       axxu81	w: max(x1 + 19, x2 + 22, x3 + 18)
 ||       #axxu72	w: max(x1 + 11, x2 + 13)
 ||       u11	w: max(x1 + 23, x2 + 29, x3 + 24)
 ||       sel	w: max(x1 + 46, x2 + 45)
 ||       u32	w: max(x1 + 8, x2 + 2)
 ||       u64	w: max(x1, x2 + 15)
 ||       afterNth	w: max(x1 + 29, x2 + 24)
 ||       #axxu62	w: max(x1 + 21, x2 + 19, x3 + 23, x4 + 20)
 ||       nil	w: 6
 ||       #axxsnd	w: x1 + 7
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: max(x2 + 14)
 ||       axxu41	w: max(x1 + 39, x2 + 42, x3 + 45)
 ||       axxafterNth	w: max(x1 + 29, x2 + 24)
 ||       mark	w: x1
 ||       u12	w: max(x1 + 27, x2 + 26, x3 + 18)
 ||       #axxu22	w: max(x1 + 11, x2 + 13)
 ||       axxu71	w: max(x1 + 4, x2 + 3)
 ||       #axxu81	w: max(x2 + 22, x3 + 22)
 ||       axxsel	w: max(x1 + 46, x2 + 45)
 ||       u72	w: max(x1 + 2, x2 + 3)
 ||       u21	w: max(x1 + 12, x2 + 3)
 ||       axxu52	w: max(x1 + 13, x2 + 14)
 ||       #axxu52	w: max(x1 + 11, x2 + 13)
 ||       axxu61	w: max(x1 + 18, x2 + 16, x3 + 15, x4 + 17)
 ||       axxfst	w: x1 + 1
 ||       u82	w: max(x1 + 14, x2 + 22, x3 + 18)
 ||       #axxu31	w: max(x2 + 18)
 ||       #axxsel	w: max(x1 + 51, x2 + 51)
 ||       #axxu42	w: max(x1 + 47, x2 + 49, x3 + 49)
 ||       axxu51	w: max(x1 + 15, x2 + 14)
 ||       head	w: x1 + 8
 ||       cons	w: max(x1 + 3, x2)
 ||       snd	w: x1 + 1
 ||       #axxu41	w: max(x1 + 48, x2 + 50, x3 + 50)
 ||       u22	w: max(x1 + 2, x2 + 3)
 ||       axxu12	w: max(x1 + 27, x2 + 26, x3 + 18)
 ||       axxtail	w: x1 + 4
 ||       u42	w: max(x1 + 43, x2 + 42, x3 + 44)
 ||       tt	w: 2
 ||       axxu42	w: max(x1 + 43, x2 + 42, x3 + 44)
 ||       u71	w: max(x1 + 4, x2 + 3)
 ||       axxtake	w: max(x1 + 22, x2 + 23)
 ||       #axxu61	w: max(x1 + 21, x2 + 19, x3 + 23, x4 + 20)
 ||       #axxfst	w: x1 + 3
 ||       #axxu71	w: max(x2 + 14)
 ||       #axxu63	w: max(x1 + 21, x2 + 19, x3 + 23, x4 + 20)
 ||       u31	w: max(x1 + 7, x2 + 10)
 ||       axxu21	w: max(x1 + 12, x2 + 3)
 ||       #axxtake	w: max(x1 + 23, x2 + 23)
 ||       #axxhead	w: x1 + 19
 ||       axxhead	w: x1 + 8
 ||     USABLE RULES: { 1..88 }
 ||     Removed DPs: #1..11 #13..29 #31..39 #41..43 #45..50 #52..82 #84..103
 || Number of SCCs: 2, DPs: 6
 ||   SCC { #12 #30 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 1
 ||       #axxu51	w: 4
 ||       #axxu32	w: 4
 ||       u62	w: x1 + x2 + 4
 ||       TIlDePAIR	w: 0
 ||       axxu62	w: x3 + 3
 ||       s 	w: x1 + 1
 ||       #axxu12	w: 3
 ||       axxu63	w: x1 + x2 + x4 + 1
 ||       #axxu82	w: 4
 ||       axxsnd	w: 2
 ||       axxu11	w: 1
 ||       axxu32	w: 3
 ||       take	w: 0
 ||       axxsplitAt	w: 3
 ||       pair	w: 3
 ||       fst	w: 0
 ||       natsFrom	w: x1 + 4
 ||       splitAt	w: 3
 ||       u52	w: 1
 ||       #axxu11	w: 4
 ||       axxu64	w: x2 + 6
 ||       u61	w: 1
 ||       axxu31	w: 3
 ||       #axxu64	w: 4
 ||       axxu72	w: x1 + 1
 ||       axxu22	w: 5
 ||       #axxsplitAt	w: 3
 ||       axxnatsFrom	w: 3
 ||       u41	w: x1 + x2 + x3 + 3
 ||       u63	w: 2
 ||       u51	w: 1
 ||       tail	w: 1
 ||       #axxafterNth	w: 4
 ||       #mark	w: x1 + 4
 ||       #axxtail	w: 4
 ||       0 	w: 3
 ||       axxu82	w: x1
 ||       #axxnatsFrom	w: 4
 ||       axxu81	w: x2 + 3
 ||       #axxu72	w: 4
 ||       u11	w: x2 + x3 + 2
 ||       sel	w: 2
 ||       u32	w: 1
 ||       u64	w: x1 + 7
 ||       afterNth	w: 4
 ||       #axxu62	w: 4
 ||       nil	w: 3
 ||       #axxsnd	w: 4
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: 4
 ||       axxu41	w: 2
 ||       axxafterNth	w: 3
 ||       mark	w: 2
 ||       u12	w: 3
 ||       #axxu22	w: 4
 ||       axxu71	w: x1 + 2
 ||       #axxu81	w: 4
 ||       axxsel	w: x2 + 1
 ||       u72	w: x2 + 2
 ||       u21	w: x2 + 1
 ||       axxu52	w: x1 + 1
 ||       #axxu52	w: 4
 ||       axxu61	w: 1
 ||       axxfst	w: x1
 ||       u82	w: 0
 ||       #axxu31	w: 4
 ||       #axxsel	w: 4
 ||       #axxu42	w: 4
 ||       axxu51	w: x2 + 3
 ||       head	w: 0
 ||       cons	w: x1 + x2 + 3
 ||       snd	w: 1
 ||       #axxu41	w: 4
 ||       u22	w: x1 + x2 + 6
 ||       axxu12	w: x2 + x3 + 3
 ||       axxtail	w: 6
 ||       u42	w: x1 + 4
 ||       tt	w: 4
 ||       axxu42	w: x2 + 3
 ||       u71	w: x2 + 3
 ||       axxtake	w: x2
 ||       #axxu61	w: 4
 ||       #axxfst	w: 3
 ||       #axxu71	w: 4
 ||       #axxu63	w: 4
 ||       u31	w: x2 + 4
 ||       axxu21	w: x1
 ||       #axxtake	w: 4
 ||       #axxhead	w: 3
 ||       axxhead	w: x1
 ||     USABLE RULES: { }
 ||     Removed DPs: #12 #30
 || Number of SCCs: 1, DPs: 4
 ||   SCC { #40 #44 #51 #83 }
 || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded.
 ||       u81	s: []	p: 3	w: x3 + 3
 ||       #axxu51	s: []	p: 0	w: x1 + 1
 ||       #axxu32	s: [1]	p: 0	w: x1
 ||       u62	s: []	p: 10	w: max(x3, x4)
 ||       TIlDePAIR	s: [1]	p: 0	w: x1
 ||       axxu62	s: []	p: 10	w: max(x3, x4)
 ||       s 	s: [1]	p: 3	w: x1
 ||       #axxu12	s: [2,3]	p: 0	w: x2 + x3
 ||       axxu63	s: []	p: 9	w: max(x3, x4)
 ||       #axxu82	s: [3,2,1]	p: 0	w: x1 + x2 + x3
 ||       axxsnd	s: []	p: 9	w: x1 + 4
 ||       axxu11	s: [3]	p: 10	w: x3 + 6
 ||       axxu32	s: []	p: 6	w: x2 + 2
 ||       take	s: []	p: 3	w: x2 + 3
 ||       axxsplitAt	s: [2]	p: 8	w: max(x2)
 ||       pair	s: []	p: 8	w: max(x1, x2)
 ||       fst	s: []	p: 5	w: x1 + 2
 ||       natsFrom	s: [1]	p: 11	w: x1 + 1
 ||       splitAt	s: [2]	p: 8	w: max(x2)
 ||       u52	s: 2
 ||       #axxu11	s: []	p: 0	w: x1 + 1
 ||       axxu64	s: []	p: 8	w: max(x1, x2)
 ||       u61	s: []	p: 10	w: max(x3, x4)
 ||       axxu31	s: [2]	p: 0	w: x2 + 4
 ||       #axxu64	s: [1,2]	p: 0	w: x1 + x2 + 1
 ||       axxu72	s: [2]	p: 6	w: x1 + x2 + 1
 ||       axxu22	s: [2]	p: 7	w: x2 + 1
 ||       #axxsplitAt	s: [1]	p: 11	w: max(x1 + 6)
 ||       axxnatsFrom	s: [1]	p: 11	w: x1 + 1
 ||       u41	s: []	p: 4	w: x3 + 13
 ||       u63	s: []	p: 9	w: max(x3, x4)
 ||       u51	s: []	p: 9	w: x2 + 4
 ||       tail	s: [1]	p: 6	w: x1 + 6
 ||       #axxafterNth	s: []	p: 0	w: x1 + 1
 ||       #mark	s: []	p: 0	w: 1
 ||       #axxtail	s: []	p: 0	w: 0
 ||       0 	s: []	p: 10	w: 0
 ||       axxu82	s: []	p: 3	w: x3 + 3
 ||       #axxnatsFrom	s: []	p: 0	w: 0
 ||       axxu81	s: []	p: 3	w: x3 + 3
 ||       #axxu72	s: [2]	p: 0	w: x2
 ||       u11	s: [3]	p: 10	w: x3 + 6
 ||       sel	s: []	p: 4	w: x2 + 14
 ||       u32	s: []	p: 6	w: x2 + 2
 ||       u64	s: []	p: 8	w: max(x1, x2)
 ||       afterNth	s: [2]	p: 3	w: x2 + 7
 ||       #axxu62	s: [2]	p: 11	w: max(x1 + 1, x2 + 6)
 ||       nil	s: []	p: 9	w: 0
 ||       #axxsnd	s: []	p: 0	w: 1
 ||       #TIlDePAIR	s: [1]	p: 0	w: x1
 ||       #axxu21	s: []	p: 0	w: x1
 ||       axxu41	s: []	p: 4	w: x3 + 13
 ||       axxafterNth	s: [2]	p: 3	w: x2 + 7
 ||       mark	s: 1
 ||       u12	s: []	p: 9	w: x3 + 5
 ||       #axxu22	s: [2]	p: 0	w: x2
 ||       axxu71	s: []	p: 5	w: x2 + 5
 ||       #axxu81	s: []	p: 0	w: x3
 ||       axxsel	s: []	p: 4	w: x2 + 14
 ||       u72	s: [2]	p: 6	w: x1 + x2 + 1
 ||       u21	s: []	p: 9	w: x2 + 1
 ||       axxu52	s: 2
 ||       #axxu52	s: []	p: 0	w: x2 + 1
 ||       axxu61	s: []	p: 10	w: max(x3, x4)
 ||       axxfst	s: []	p: 5	w: x1 + 2
 ||       u82	s: []	p: 3	w: x3 + 3
 ||       #axxu31	s: []	p: 0	w: 1
 ||       #axxsel	s: [1,2]	p: 0	w: x1 + x2
 ||       #axxu42	s: []	p: 0	w: x3
 ||       axxu51	s: []	p: 9	w: x2 + 4
 ||       head	s: []	p: 1	w: x1 + 5
 ||       cons	s: []	p: 10	w: max(x1, x2)
 ||       snd	s: []	p: 9	w: x1 + 4
 ||       #axxu41	s: [3]	p: 0	w: x3 + 1
 ||       u22	s: [2]	p: 7	w: x2 + 1
 ||       axxu12	s: []	p: 9	w: x3 + 5
 ||       axxtail	s: [1]	p: 6	w: x1 + 6
 ||       u42	s: []	p: 2	w: x3 + 13
 ||       tt	s: []	p: 4	w: 3
 ||       axxu42	s: []	p: 2	w: x3 + 13
 ||       u71	s: []	p: 5	w: x2 + 5
 ||       axxtake	s: []	p: 3	w: x2 + 3
 ||       #axxu61	s: [2]	p: 11	w: max(x1 + 3, x2 + 6)
 ||       #axxfst	s: []	p: 0	w: 1
 ||       #axxu71	s: []	p: 0	w: x2
 ||       #axxu63	s: [2]	p: 11	w: max(x1 + 2, x2 + 6)
 ||       u31	s: [2]	p: 0	w: x2 + 4
 ||       axxu21	s: []	p: 9	w: x2 + 1
 ||       #axxtake	s: []	p: 0	w: x1 + 1
 ||       #axxhead	s: []	p: 0	w: 1
 ||       axxhead	s: []	p: 1	w: x1 + 5
 ||     USABLE RULES: { 1..88 }
 ||     Removed DPs: #83
 || 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] map#(/\x.X(x), cons(Y, Z)) =#> map#(/\y.X(y), Z)   

  Rules R_0:

    axxu11(tt, X, Y) => axxu12(tt, X, Y) 
    axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxu21(tt, X) => axxu22(tt, X) 
    axxu22(tt, X) => mark(X) 
    axxu31(tt, X) => axxu32(tt, X) 
    axxu32(tt, X) => mark(X) 
    axxu41(tt, X, Y) => axxu42(tt, X, Y) 
    axxu42(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxu51(tt, X) => axxu52(tt, X) 
    axxu52(tt, X) => mark(X) 
    axxu61(tt, X, Y, Z) => axxu62(tt, X, Y, Z) 
    axxu62(tt, X, Y, Z) => axxu63(tt, X, Y, Z) 
    axxu63(tt, X, Y, Z) => axxu64(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu64(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxu71(tt, X) => axxu72(tt, X) 
    axxu72(tt, X) => mark(X) 
    axxu81(tt, X, Y) => axxu82(tt, X, Y) 
    axxu82(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    axxafterNth(X, Y) => axxu11(tt, X, Y) 
    axxfst(pair(X, Y)) => axxu21(tt, X) 
    axxhead(cons(X, Y)) => axxu31(tt, X) 
    axxnatsFrom(X) => cons(mark(X), natsFrom(s(X))) 
    axxsel(X, Y) => axxu41(tt, X, Y) 
    axxsnd(pair(X, Y)) => axxu51(tt, Y) 
    axxsplitAt(0, X) => pair(nil, mark(X)) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu61(tt, X, Y, Z) 
    axxtail(cons(X, Y)) => axxu71(tt, Y) 
    axxtake(X, Y) => axxu81(tt, X, Y) 
    mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
    mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(u21(X, Y)) => axxu21(mark(X), Y) 
    mark(u22(X, Y)) => axxu22(mark(X), Y) 
    mark(u31(X, Y)) => axxu31(mark(X), Y) 
    mark(u32(X, Y)) => axxu32(mark(X), Y) 
    mark(u41(X, Y, Z)) => axxu41(mark(X), Y, Z) 
    mark(u42(X, Y, Z)) => axxu42(mark(X), Y, Z) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(u51(X, Y)) => axxu51(mark(X), Y) 
    mark(u52(X, Y)) => axxu52(mark(X), Y) 
    mark(u61(X, Y, Z, U)) => axxu61(mark(X), Y, Z, U) 
    mark(u62(X, Y, Z, U)) => axxu62(mark(X), Y, Z, U) 
    mark(u63(X, Y, Z, U)) => axxu63(mark(X), Y, Z, U) 
    mark(u64(X, Y)) => axxu64(mark(X), Y) 
    mark(u71(X, Y)) => axxu71(mark(X), Y) 
    mark(u72(X, Y)) => axxu72(mark(X), Y) 
    mark(u81(X, Y, Z)) => axxu81(mark(X), Y, Z) 
    mark(u82(X, Y, Z)) => axxu82(mark(X), Y, Z) 
    mark(fst(X)) => axxfst(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) => u11(X, Y, Z) 
    axxu12(X, Y, Z) => u12(X, Y, Z) 
    axxsnd(X) => snd(X) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxu21(X, Y) => u21(X, Y) 
    axxu22(X, Y) => u22(X, Y) 
    axxu31(X, Y) => u31(X, Y) 
    axxu32(X, Y) => u32(X, Y) 
    axxu41(X, Y, Z) => u41(X, Y, Z) 
    axxu42(X, Y, Z) => u42(X, Y, Z) 
    axxhead(X) => head(X) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxu51(X, Y) => u51(X, Y) 
    axxu52(X, Y) => u52(X, Y) 
    axxu61(X, Y, Z, U) => u61(X, Y, Z, U) 
    axxu62(X, Y, Z, U) => u62(X, Y, Z, U) 
    axxu63(X, Y, Z, U) => u63(X, Y, Z, U) 
    axxu64(X, Y) => u64(X, Y) 
    axxu71(X, Y) => u71(X, Y) 
    axxu72(X, Y) => u72(X, Y) 
    axxu81(X, Y, Z) => u81(X, Y, Z) 
    axxu82(X, Y, Z) => u82(X, Y, Z) 
    axxfst(X) => fst(X) 
    axxnatsFrom(X) => natsFrom(X) 
    axxsel(X, Y) => sel(X, Y) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    map(/\x.X(x), nil) => nil 
    map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    app(/\x.X(x), Y) => X(Y) 

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(map#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(map#(/\x.X(x), cons(Y, Z))) = cons(Y, Z) |> Z = nu(map#(/\y.X(y), Z)) 

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.