We consider the system h32.

  Alphabet:

    0 : [] --> A 
    afterNth : [] --> A -> A -> A 
    and : [] --> A -> A -> A 
    app : [] --> (A -> A) -> A -> A 
    axxafterNth : [] --> A -> A -> A 
    axxand : [] --> A -> A -> A 
    axxfst : [] --> A -> A 
    axxhead : [] --> A -> A 
    axxisLNat : [] --> A -> A 
    axxisNatural : [] --> A -> A 
    axxisPLNat : [] --> A -> A 
    axxnatsFrom : [] --> A -> A 
    axxsel : [] --> A -> A -> A 
    axxsnd : [] --> A -> A 
    axxsplitAt : [] --> A -> A -> A 
    axxtail : [] --> A -> A 
    axxtake : [] --> A -> A -> A 
    axxu101 : [] --> A -> A -> A -> A 
    axxu11 : [] --> A -> A -> A -> A 
    axxu21 : [] --> A -> A -> A 
    axxu31 : [] --> A -> A -> A 
    axxu41 : [] --> A -> A -> A 
    axxu51 : [] --> A -> A -> A -> A 
    axxu61 : [] --> A -> A -> A 
    axxu71 : [] --> A -> A -> A 
    axxu81 : [] --> A -> A -> A -> A -> A 
    axxu82 : [] --> A -> A -> A 
    axxu91 : [] --> A -> A -> A 
    cons : [] --> A -> A -> A 
    fst : [] --> A -> A 
    head : [] --> A -> A 
    isLNat : [] --> A -> A 
    isNatural : [] --> A -> A 
    isPLNat : [] --> 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 
    u101 : [] --> A -> A -> A -> A 
    u11 : [] --> A -> A -> A -> A 
    u21 : [] --> A -> A -> A 
    u31 : [] --> A -> A -> A 
    u41 : [] --> A -> A -> A 
    u51 : [] --> A -> A -> A -> A 
    u61 : [] --> A -> A -> A 
    u71 : [] --> A -> A -> A 
    u81 : [] --> A -> A -> A -> A -> A 
    u82 : [] --> A -> A -> A 
    u91 : [] --> A -> A -> A 

  Rules:

    axxu101 tt x y => axxfst (axxsplitAt (mark x) (mark y)) 
    axxu11 tt x y => axxsnd (axxsplitAt (mark x) (mark y)) 
    axxu21 tt x => mark x 
    axxu31 tt x => mark x 
    axxu41 tt x => cons (mark x) (natsFrom (s x)) 
    axxu51 tt x y => axxhead (axxafterNth (mark x) (mark y)) 
    axxu61 tt x => mark x 
    axxu71 tt x => pair nil (mark x) 
    axxu81 tt x y z => axxu82 (axxsplitAt (mark x) (mark z)) y 
    axxu82 (pair x y) z => pair (cons (mark z) x) (mark y) 
    axxu91 tt x => mark x 
    axxafterNth x y => axxu11 (axxand (axxisNatural x) (isLNat y)) x y 
    axxand tt x => mark x 
    axxfst (pair x y) => axxu21 (axxand (axxisLNat x) (isLNat y)) x 
    axxhead (cons x y) => axxu31 (axxand (axxisNatural x) (isLNat y)) x 
    axxisLNat nil => tt 
    axxisLNat (afterNth x y) => axxand (axxisNatural x) (isLNat y) 
    axxisLNat (cons x y) => axxand (axxisNatural x) (isLNat y) 
    axxisLNat (fst x) => axxisPLNat x 
    axxisLNat (natsFrom x) => axxisNatural x 
    axxisLNat (snd x) => axxisPLNat x 
    axxisLNat (tail x) => axxisLNat x 
    axxisLNat (take x y) => axxand (axxisNatural x) (isLNat y) 
    axxisNatural 0 => tt 
    axxisNatural (head x) => axxisLNat x 
    axxisNatural (s x) => axxisNatural x 
    axxisNatural (sel x y) => axxand (axxisNatural x) (isLNat y) 
    axxisPLNat (pair x y) => axxand (axxisLNat x) (isLNat y) 
    axxisPLNat (splitAt x y) => axxand (axxisNatural x) (isLNat y) 
    axxnatsFrom x => axxu41 (axxisNatural x) x 
    axxsel x y => axxu51 (axxand (axxisNatural x) (isLNat y)) x y 
    axxsnd (pair x y) => axxu61 (axxand (axxisLNat x) (isLNat y)) y 
    axxsplitAt 0 x => axxu71 (axxisLNat x) x 
    axxsplitAt (s x) (cons y z) => axxu81 (axxand (axxisNatural x) (and (isNatural y) (isLNat z))) x y z 
    axxtail (cons x y) => axxu91 (axxand (axxisNatural x) (isLNat y)) y 
    axxtake x y => axxu101 (axxand (axxisNatural x) (isLNat y)) x y 
    mark (u101 x y z) => axxu101 (mark x) y z 
    mark (fst x) => axxfst (mark x) 
    mark (splitAt x y) => axxsplitAt (mark x) (mark y) 
    mark (u11 x y z) => axxu11 (mark x) y z 
    mark (snd x) => axxsnd (mark x) 
    mark (u21 x y) => axxu21 (mark x) y 
    mark (u31 x y) => axxu31 (mark x) y 
    mark (u41 x y) => axxu41 (mark x) y 
    mark (natsFrom x) => axxnatsFrom (mark x) 
    mark (u51 x y z) => axxu51 (mark x) y z 
    mark (head x) => axxhead (mark x) 
    mark (afterNth x y) => axxafterNth (mark x) (mark y) 
    mark (u61 x y) => axxu61 (mark x) y 
    mark (u71 x y) => axxu71 (mark x) y 
    mark (u81 x y z u) => axxu81 (mark x) y z u 
    mark (u82 x y) => axxu82 (mark x) y 
    mark (u91 x y) => axxu91 (mark x) y 
    mark (and x y) => axxand (mark x) y 
    mark (isNatural x) => axxisNatural x 
    mark (isLNat x) => axxisLNat x 
    mark (isPLNat x) => axxisPLNat x 
    mark (tail x) => axxtail (mark x) 
    mark (take x y) => axxtake (mark x) (mark y) 
    mark (sel x y) => axxsel (mark x) (mark y) 
    mark tt => tt 
    mark (cons x y) => cons (mark x) y 
    mark (s x) => s (mark x) 
    mark (pair x y) => pair (mark x) (mark y) 
    mark nil => nil 
    mark 0 => 0 
    axxu101 x y z => u101 x y z 
    axxfst x => fst x 
    axxsplitAt x y => splitAt x y 
    axxu11 x y z => u11 x y z 
    axxsnd x => snd x 
    axxu21 x y => u21 x y 
    axxu31 x y => u31 x y 
    axxu41 x y => u41 x y 
    axxnatsFrom x => natsFrom x 
    axxu51 x y z => u51 x y z 
    axxhead x => head x 
    axxafterNth x y => afterNth x y 
    axxu61 x y => u61 x y 
    axxu71 x y => u71 x y 
    axxu81 x y z u => u81 x y z u 
    axxu82 x y => u82 x y 
    axxu91 x y => u91 x y 
    axxand x y => and x y 
    axxisNatural x => isNatural x 
    axxisLNat x => isLNat x 
    axxisPLNat x => isPLNat x 
    axxtail x => tail x 
    axxtake x y => take x y 
    axxsel x y => sel x y 
    map (/\x.f x) nil => nil 
    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 
    and : [A * A] --> A 
    app : [A -> A * A] --> A 
    axxafterNth : [A * A] --> A 
    axxand : [A * A] --> A 
    axxfst : [A] --> A 
    axxhead : [A] --> A 
    axxisLNat : [A] --> A 
    axxisNatural : [A] --> A 
    axxisPLNat : [A] --> A 
    axxnatsFrom : [A] --> A 
    axxsel : [A * A] --> A 
    axxsnd : [A] --> A 
    axxsplitAt : [A * A] --> A 
    axxtail : [A] --> A 
    axxtake : [A * A] --> A 
    axxu101 : [A * A * A] --> A 
    axxu11 : [A * A * A] --> A 
    axxu21 : [A * A] --> A 
    axxu31 : [A * A] --> A 
    axxu41 : [A * A] --> A 
    axxu51 : [A * A * A] --> A 
    axxu61 : [A * A] --> A 
    axxu71 : [A * A] --> A 
    axxu81 : [A * A * A * A] --> A 
    axxu82 : [A * A] --> A 
    axxu91 : [A * A] --> A 
    cons : [A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    isLNat : [A] --> A 
    isNatural : [A] --> A 
    isPLNat : [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 
    u101 : [A * A * A] --> A 
    u11 : [A * A * A] --> A 
    u21 : [A * A] --> A 
    u31 : [A * A] --> A 
    u41 : [A * A] --> A 
    u51 : [A * A * A] --> A 
    u61 : [A * A] --> A 
    u71 : [A * A] --> A 
    u81 : [A * A * A * A] --> A 
    u82 : [A * A] --> A 
    u91 : [A * A] --> A 
    ~AP1 : [A -> A * A] --> A 

  Rules:

    axxu101(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    axxu11(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxu21(tt, X) => mark(X) 
    axxu31(tt, X) => mark(X) 
    axxu41(tt, X) => cons(mark(X), natsFrom(s(X))) 
    axxu51(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxu61(tt, X) => mark(X) 
    axxu71(tt, X) => pair(nil, mark(X)) 
    axxu81(tt, X, Y, Z) => axxu82(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu82(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxu91(tt, X) => mark(X) 
    axxafterNth(X, Y) => axxu11(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    axxand(tt, X) => mark(X) 
    axxfst(pair(X, Y)) => axxu21(axxand(axxisLNat(X), isLNat(Y)), X) 
    axxhead(cons(X, Y)) => axxu31(axxand(axxisNatural(X), isLNat(Y)), X) 
    axxisLNat(nil) => tt 
    axxisLNat(afterNth(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisLNat(cons(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisLNat(fst(X)) => axxisPLNat(X) 
    axxisLNat(natsFrom(X)) => axxisNatural(X) 
    axxisLNat(snd(X)) => axxisPLNat(X) 
    axxisLNat(tail(X)) => axxisLNat(X) 
    axxisLNat(take(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisNatural(0) => tt 
    axxisNatural(head(X)) => axxisLNat(X) 
    axxisNatural(s(X)) => axxisNatural(X) 
    axxisNatural(sel(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisPLNat(pair(X, Y)) => axxand(axxisLNat(X), isLNat(Y)) 
    axxisPLNat(splitAt(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxnatsFrom(X) => axxu41(axxisNatural(X), X) 
    axxsel(X, Y) => axxu51(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    axxsnd(pair(X, Y)) => axxu61(axxand(axxisLNat(X), isLNat(Y)), Y) 
    axxsplitAt(0, X) => axxu71(axxisLNat(X), X) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu81(axxand(axxisNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z) 
    axxtail(cons(X, Y)) => axxu91(axxand(axxisNatural(X), isLNat(Y)), Y) 
    axxtake(X, Y) => axxu101(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    mark(u101(X, Y, Z)) => axxu101(mark(X), Y, Z) 
    mark(fst(X)) => axxfst(mark(X)) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(u21(X, Y)) => axxu21(mark(X), Y) 
    mark(u31(X, Y)) => axxu31(mark(X), Y) 
    mark(u41(X, Y)) => axxu41(mark(X), Y) 
    mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
    mark(u51(X, Y, Z)) => axxu51(mark(X), Y, Z) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(u61(X, Y)) => axxu61(mark(X), Y) 
    mark(u71(X, Y)) => axxu71(mark(X), Y) 
    mark(u81(X, Y, Z, U)) => axxu81(mark(X), Y, Z, U) 
    mark(u82(X, Y)) => axxu82(mark(X), Y) 
    mark(u91(X, Y)) => axxu91(mark(X), Y) 
    mark(and(X, Y)) => axxand(mark(X), Y) 
    mark(isNatural(X)) => axxisNatural(X) 
    mark(isLNat(X)) => axxisLNat(X) 
    mark(isPLNat(X)) => axxisPLNat(X) 
    mark(tail(X)) => axxtail(mark(X)) 
    mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
    mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
    mark(tt) => tt 
    mark(cons(X, Y)) => cons(mark(X), Y) 
    mark(s(X)) => s(mark(X)) 
    mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
    mark(nil) => nil 
    mark(0) => 0 
    axxu101(X, Y, Z) => u101(X, Y, Z) 
    axxfst(X) => fst(X) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxu11(X, Y, Z) => u11(X, Y, Z) 
    axxsnd(X) => snd(X) 
    axxu21(X, Y) => u21(X, Y) 
    axxu31(X, Y) => u31(X, Y) 
    axxu41(X, Y) => u41(X, Y) 
    axxnatsFrom(X) => natsFrom(X) 
    axxu51(X, Y, Z) => u51(X, Y, Z) 
    axxhead(X) => head(X) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxu61(X, Y) => u61(X, Y) 
    axxu71(X, Y) => u71(X, Y) 
    axxu81(X, Y, Z, U) => u81(X, Y, Z, U) 
    axxu82(X, Y) => u82(X, Y) 
    axxu91(X, Y) => u91(X, Y) 
    axxand(X, Y) => and(X, Y) 
    axxisNatural(X) => isNatural(X) 
    axxisLNat(X) => isLNat(X) 
    axxisPLNat(X) => isPLNat(X) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    axxsel(X, Y) => sel(X, Y) 
    map(/\x.~AP1(F, x), nil) => nil 
    app(/\x.~AP1(F, x), X) => ~AP1(F, X) 
    map(/\x.afterNth(X, x), nil) => nil 
    map(/\x.and(X, x), nil) => nil 
    map(/\x.app(F, x), nil) => nil 
    map(/\x.axxafterNth(X, x), nil) => nil 
    map(/\x.axxand(X, x), nil) => nil 
    map(/\x.axxfst(x), nil) => nil 
    map(/\x.axxhead(x), nil) => nil 
    map(/\x.axxisLNat(x), nil) => nil 
    map(/\x.axxisNatural(x), nil) => nil 
    map(/\x.axxisPLNat(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.axxu101(X, Y, x), nil) => nil 
    map(/\x.axxu11(X, Y, x), nil) => nil 
    map(/\x.axxu21(X, x), nil) => nil 
    map(/\x.axxu31(X, x), nil) => nil 
    map(/\x.axxu41(X, x), nil) => nil 
    map(/\x.axxu51(X, Y, x), nil) => nil 
    map(/\x.axxu61(X, x), nil) => nil 
    map(/\x.axxu71(X, x), nil) => nil 
    map(/\x.axxu81(X, Y, Z, x), nil) => nil 
    map(/\x.axxu82(X, x), nil) => nil 
    map(/\x.axxu91(X, x), nil) => nil 
    map(/\x.cons(X, x), nil) => nil 
    map(/\x.fst(x), nil) => nil 
    map(/\x.head(x), nil) => nil 
    map(/\x.isLNat(x), nil) => nil 
    map(/\x.isNatural(x), nil) => nil 
    map(/\x.isPLNat(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.u101(X, Y, x), nil) => nil 
    map(/\x.u11(X, Y, x), nil) => nil 
    map(/\x.u21(X, x), nil) => nil 
    map(/\x.u31(X, x), nil) => nil 
    map(/\x.u41(X, x), nil) => nil 
    map(/\x.u51(X, Y, x), nil) => nil 
    map(/\x.u61(X, x), nil) => nil 
    map(/\x.u71(X, x), nil) => nil 
    map(/\x.u81(X, Y, Z, x), nil) => nil 
    map(/\x.u82(X, x), nil) => nil 
    map(/\x.u91(X, x), nil) => nil 
    app(/\x.afterNth(X, x), Y) => afterNth(X, Y) 
    app(/\x.and(X, x), Y) => and(X, Y) 
    app(/\x.app(F, x), X) => app(F, X) 
    app(/\x.axxafterNth(X, x), Y) => axxafterNth(X, Y) 
    app(/\x.axxand(X, x), Y) => axxand(X, Y) 
    app(/\x.axxfst(x), X) => axxfst(X) 
    app(/\x.axxhead(x), X) => axxhead(X) 
    app(/\x.axxisLNat(x), X) => axxisLNat(X) 
    app(/\x.axxisNatural(x), X) => axxisNatural(X) 
    app(/\x.axxisPLNat(x), X) => axxisPLNat(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.axxu101(X, Y, x), Z) => axxu101(X, Y, Z) 
    app(/\x.axxu11(X, Y, x), Z) => axxu11(X, Y, Z) 
    app(/\x.axxu21(X, x), Y) => axxu21(X, Y) 
    app(/\x.axxu31(X, x), Y) => axxu31(X, Y) 
    app(/\x.axxu41(X, x), Y) => axxu41(X, Y) 
    app(/\x.axxu51(X, Y, x), Z) => axxu51(X, Y, Z) 
    app(/\x.axxu61(X, x), Y) => axxu61(X, Y) 
    app(/\x.axxu71(X, x), Y) => axxu71(X, Y) 
    app(/\x.axxu81(X, Y, Z, x), U) => axxu81(X, Y, Z, U) 
    app(/\x.axxu82(X, x), Y) => axxu82(X, Y) 
    app(/\x.axxu91(X, x), Y) => axxu91(X, Y) 
    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.isLNat(x), X) => isLNat(X) 
    app(/\x.isNatural(x), X) => isNatural(X) 
    app(/\x.isPLNat(x), X) => isPLNat(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.u101(X, Y, x), Z) => u101(X, Y, Z) 
    app(/\x.u11(X, Y, x), Z) => u11(X, Y, Z) 
    app(/\x.u21(X, x), Y) => u21(X, Y) 
    app(/\x.u31(X, x), Y) => u31(X, Y) 
    app(/\x.u41(X, x), Y) => u41(X, Y) 
    app(/\x.u51(X, Y, x), Z) => u51(X, Y, Z) 
    app(/\x.u61(X, x), Y) => u61(X, Y) 
    app(/\x.u71(X, x), Y) => u71(X, Y) 
    app(/\x.u81(X, Y, Z, x), U) => u81(X, Y, Z, U) 
    app(/\x.u82(X, x), Y) => u82(X, Y) 
    app(/\x.u91(X, x), Y) => u91(X, Y) 
    ~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 
    app : [A -> A * A] --> A 
    axxafterNth : [A * A] --> A 
    axxand : [A * A] --> A 
    axxfst : [A] --> A 
    axxhead : [A] --> A 
    axxisLNat : [A] --> A 
    axxisNatural : [A] --> A 
    axxisPLNat : [A] --> A 
    axxnatsFrom : [A] --> A 
    axxsel : [A * A] --> A 
    axxsnd : [A] --> A 
    axxsplitAt : [A * A] --> A 
    axxtail : [A] --> A 
    axxtake : [A * A] --> A 
    axxu101 : [A * A * A] --> A 
    axxu11 : [A * A * A] --> A 
    axxu21 : [A * A] --> A 
    axxu31 : [A * A] --> A 
    axxu41 : [A * A] --> A 
    axxu51 : [A * A * A] --> A 
    axxu61 : [A * A] --> A 
    axxu71 : [A * A] --> A 
    axxu81 : [A * A * A * A] --> A 
    axxu82 : [A * A] --> A 
    axxu91 : [A * A] --> A 
    cons : [A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    isLNat : [A] --> A 
    isNatural : [A] --> A 
    isPLNat : [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 
    u101 : [A * A * A] --> A 
    u11 : [A * A * A] --> A 
    u21 : [A * A] --> A 
    u31 : [A * A] --> A 
    u41 : [A * A] --> A 
    u51 : [A * A * A] --> A 
    u61 : [A * A] --> A 
    u71 : [A * A] --> A 
    u81 : [A * A * A * A] --> A 
    u82 : [A * A] --> A 
    u91 : [A * A] --> A 

  Rules:

    axxu101(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    axxu11(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxu21(tt, X) => mark(X) 
    axxu31(tt, X) => mark(X) 
    axxu41(tt, X) => cons(mark(X), natsFrom(s(X))) 
    axxu51(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxu61(tt, X) => mark(X) 
    axxu71(tt, X) => pair(nil, mark(X)) 
    axxu81(tt, X, Y, Z) => axxu82(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu82(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxu91(tt, X) => mark(X) 
    axxafterNth(X, Y) => axxu11(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    axxand(tt, X) => mark(X) 
    axxfst(pair(X, Y)) => axxu21(axxand(axxisLNat(X), isLNat(Y)), X) 
    axxhead(cons(X, Y)) => axxu31(axxand(axxisNatural(X), isLNat(Y)), X) 
    axxisLNat(nil) => tt 
    axxisLNat(afterNth(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisLNat(cons(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisLNat(fst(X)) => axxisPLNat(X) 
    axxisLNat(natsFrom(X)) => axxisNatural(X) 
    axxisLNat(snd(X)) => axxisPLNat(X) 
    axxisLNat(tail(X)) => axxisLNat(X) 
    axxisLNat(take(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisNatural(0) => tt 
    axxisNatural(head(X)) => axxisLNat(X) 
    axxisNatural(s(X)) => axxisNatural(X) 
    axxisNatural(sel(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisPLNat(pair(X, Y)) => axxand(axxisLNat(X), isLNat(Y)) 
    axxisPLNat(splitAt(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxnatsFrom(X) => axxu41(axxisNatural(X), X) 
    axxsel(X, Y) => axxu51(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    axxsnd(pair(X, Y)) => axxu61(axxand(axxisLNat(X), isLNat(Y)), Y) 
    axxsplitAt(0, X) => axxu71(axxisLNat(X), X) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu81(axxand(axxisNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z) 
    axxtail(cons(X, Y)) => axxu91(axxand(axxisNatural(X), isLNat(Y)), Y) 
    axxtake(X, Y) => axxu101(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    mark(u101(X, Y, Z)) => axxu101(mark(X), Y, Z) 
    mark(fst(X)) => axxfst(mark(X)) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(u21(X, Y)) => axxu21(mark(X), Y) 
    mark(u31(X, Y)) => axxu31(mark(X), Y) 
    mark(u41(X, Y)) => axxu41(mark(X), Y) 
    mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
    mark(u51(X, Y, Z)) => axxu51(mark(X), Y, Z) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(u61(X, Y)) => axxu61(mark(X), Y) 
    mark(u71(X, Y)) => axxu71(mark(X), Y) 
    mark(u81(X, Y, Z, U)) => axxu81(mark(X), Y, Z, U) 
    mark(u82(X, Y)) => axxu82(mark(X), Y) 
    mark(u91(X, Y)) => axxu91(mark(X), Y) 
    mark(and(X, Y)) => axxand(mark(X), Y) 
    mark(isNatural(X)) => axxisNatural(X) 
    mark(isLNat(X)) => axxisLNat(X) 
    mark(isPLNat(X)) => axxisPLNat(X) 
    mark(tail(X)) => axxtail(mark(X)) 
    mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
    mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
    mark(tt) => tt 
    mark(cons(X, Y)) => cons(mark(X), Y) 
    mark(s(X)) => s(mark(X)) 
    mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
    mark(nil) => nil 
    mark(0) => 0 
    axxu101(X, Y, Z) => u101(X, Y, Z) 
    axxfst(X) => fst(X) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxu11(X, Y, Z) => u11(X, Y, Z) 
    axxsnd(X) => snd(X) 
    axxu21(X, Y) => u21(X, Y) 
    axxu31(X, Y) => u31(X, Y) 
    axxu41(X, Y) => u41(X, Y) 
    axxnatsFrom(X) => natsFrom(X) 
    axxu51(X, Y, Z) => u51(X, Y, Z) 
    axxhead(X) => head(X) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxu61(X, Y) => u61(X, Y) 
    axxu71(X, Y) => u71(X, Y) 
    axxu81(X, Y, Z, U) => u81(X, Y, Z, U) 
    axxu82(X, Y) => u82(X, Y) 
    axxu91(X, Y) => u91(X, Y) 
    axxand(X, Y) => and(X, Y) 
    axxisNatural(X) => isNatural(X) 
    axxisLNat(X) => isLNat(X) 
    axxisPLNat(X) => isPLNat(X) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    axxsel(X, Y) => sel(X, Y) 
    map(/\x.X(x), nil) => nil 
    app(/\x.X(x), Y) => X(Y) 

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

  axxu101(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
  axxu11(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
  axxu21(tt, X) => mark(X) 
  axxu31(tt, X) => mark(X) 
  axxu41(tt, X) => cons(mark(X), natsFrom(s(X))) 
  axxu51(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
  axxu61(tt, X) => mark(X) 
  axxu71(tt, X) => pair(nil, mark(X)) 
  axxu81(tt, X, Y, Z) => axxu82(axxsplitAt(mark(X), mark(Z)), Y) 
  axxu82(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
  axxu91(tt, X) => mark(X) 
  axxafterNth(X, Y) => axxu11(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
  axxand(tt, X) => mark(X) 
  axxfst(pair(X, Y)) => axxu21(axxand(axxisLNat(X), isLNat(Y)), X) 
  axxhead(cons(X, Y)) => axxu31(axxand(axxisNatural(X), isLNat(Y)), X) 
  axxisLNat(nil) => tt 
  axxisLNat(afterNth(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
  axxisLNat(cons(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
  axxisLNat(fst(X)) => axxisPLNat(X) 
  axxisLNat(natsFrom(X)) => axxisNatural(X) 
  axxisLNat(snd(X)) => axxisPLNat(X) 
  axxisLNat(tail(X)) => axxisLNat(X) 
  axxisLNat(take(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
  axxisNatural(0) => tt 
  axxisNatural(head(X)) => axxisLNat(X) 
  axxisNatural(s(X)) => axxisNatural(X) 
  axxisNatural(sel(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
  axxisPLNat(pair(X, Y)) => axxand(axxisLNat(X), isLNat(Y)) 
  axxisPLNat(splitAt(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
  axxnatsFrom(X) => axxu41(axxisNatural(X), X) 
  axxsel(X, Y) => axxu51(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
  axxsnd(pair(X, Y)) => axxu61(axxand(axxisLNat(X), isLNat(Y)), Y) 
  axxsplitAt(0, X) => axxu71(axxisLNat(X), X) 
  axxsplitAt(s(X), cons(Y, Z)) => axxu81(axxand(axxisNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z) 
  axxtail(cons(X, Y)) => axxu91(axxand(axxisNatural(X), isLNat(Y)), Y) 
  axxtake(X, Y) => axxu101(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
  mark(u101(X, Y, Z)) => axxu101(mark(X), Y, Z) 
  mark(fst(X)) => axxfst(mark(X)) 
  mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
  mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
  mark(snd(X)) => axxsnd(mark(X)) 
  mark(u21(X, Y)) => axxu21(mark(X), Y) 
  mark(u31(X, Y)) => axxu31(mark(X), Y) 
  mark(u41(X, Y)) => axxu41(mark(X), Y) 
  mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
  mark(u51(X, Y, Z)) => axxu51(mark(X), Y, Z) 
  mark(head(X)) => axxhead(mark(X)) 
  mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
  mark(u61(X, Y)) => axxu61(mark(X), Y) 
  mark(u71(X, Y)) => axxu71(mark(X), Y) 
  mark(u81(X, Y, Z, U)) => axxu81(mark(X), Y, Z, U) 
  mark(u82(X, Y)) => axxu82(mark(X), Y) 
  mark(u91(X, Y)) => axxu91(mark(X), Y) 
  mark(and(X, Y)) => axxand(mark(X), Y) 
  mark(isNatural(X)) => axxisNatural(X) 
  mark(isLNat(X)) => axxisLNat(X) 
  mark(isPLNat(X)) => axxisPLNat(X) 
  mark(tail(X)) => axxtail(mark(X)) 
  mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
  mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
  mark(tt) => tt 
  mark(cons(X, Y)) => cons(mark(X), Y) 
  mark(s(X)) => s(mark(X)) 
  mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
  mark(nil) => nil 
  mark(0) => 0 
  axxu101(X, Y, Z) => u101(X, Y, Z) 
  axxfst(X) => fst(X) 
  axxsplitAt(X, Y) => splitAt(X, Y) 
  axxu11(X, Y, Z) => u11(X, Y, Z) 
  axxsnd(X) => snd(X) 
  axxu21(X, Y) => u21(X, Y) 
  axxu31(X, Y) => u31(X, Y) 
  axxu41(X, Y) => u41(X, Y) 
  axxnatsFrom(X) => natsFrom(X) 
  axxu51(X, Y, Z) => u51(X, Y, Z) 
  axxhead(X) => head(X) 
  axxafterNth(X, Y) => afterNth(X, Y) 
  axxu61(X, Y) => u61(X, Y) 
  axxu71(X, Y) => u71(X, Y) 
  axxu81(X, Y, Z, U) => u81(X, Y, Z, U) 
  axxu82(X, Y) => u82(X, Y) 
  axxu91(X, Y) => u91(X, Y) 
  axxand(X, Y) => and(X, Y) 
  axxisNatural(X) => isNatural(X) 
  axxisLNat(X) => isLNat(X) 
  axxisPLNat(X) => isPLNat(X) 
  axxtail(X) => tail(X) 
  axxtake(X, Y) => take(X, Y) 
  axxsel(X, Y) => sel(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: axxu101(tt(),PeRCenTX,PeRCenTY) -> axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     2: axxu11(tt(),PeRCenTX,PeRCenTY) -> axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     3: axxu21(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     4: axxu31(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     5: axxu41(tt(),PeRCenTX) -> cons(mark(PeRCenTX),natsFrom(s(PeRCenTX)))
 ||     6: axxu51(tt(),PeRCenTX,PeRCenTY) -> axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||     7: axxu61(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     8: axxu71(tt(),PeRCenTX) -> pair(nil(),mark(PeRCenTX))
 ||     9: axxu81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu82(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY)
 ||     10: axxu82(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> pair(cons(mark(PeRCenTZ),PeRCenTX),mark(PeRCenTY))
 ||     11: axxu91(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     12: axxafterNth(PeRCenTX,PeRCenTY) -> axxu11(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||     13: axxand(tt(),PeRCenTX) -> mark(PeRCenTX)
 ||     14: axxfst(pair(PeRCenTX,PeRCenTY)) -> axxu21(axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX)
 ||     15: axxhead(cons(PeRCenTX,PeRCenTY)) -> axxu31(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX)
 ||     16: axxisLNat(nil()) -> tt()
 ||     17: axxisLNat(afterNth(PeRCenTX,PeRCenTY)) -> axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||     18: axxisLNat(cons(PeRCenTX,PeRCenTY)) -> axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||     19: axxisLNat(fst(PeRCenTX)) -> axxisPLNat(PeRCenTX)
 ||     20: axxisLNat(natsFrom(PeRCenTX)) -> axxisNatural(PeRCenTX)
 ||     21: axxisLNat(snd(PeRCenTX)) -> axxisPLNat(PeRCenTX)
 ||     22: axxisLNat(tail(PeRCenTX)) -> axxisLNat(PeRCenTX)
 ||     23: axxisLNat(take(PeRCenTX,PeRCenTY)) -> axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||     24: axxisNatural(0()) -> tt()
 ||     25: axxisNatural(head(PeRCenTX)) -> axxisLNat(PeRCenTX)
 ||     26: axxisNatural(s(PeRCenTX)) -> axxisNatural(PeRCenTX)
 ||     27: axxisNatural(sel(PeRCenTX,PeRCenTY)) -> axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||     28: axxisPLNat(pair(PeRCenTX,PeRCenTY)) -> axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY))
 ||     29: axxisPLNat(splitAt(PeRCenTX,PeRCenTY)) -> axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||     30: axxnatsFrom(PeRCenTX) -> axxu41(axxisNatural(PeRCenTX),PeRCenTX)
 ||     31: axxsel(PeRCenTX,PeRCenTY) -> axxu51(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||     32: axxsnd(pair(PeRCenTX,PeRCenTY)) -> axxu61(axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY)
 ||     33: axxsplitAt(0(),PeRCenTX) -> axxu71(axxisLNat(PeRCenTX),PeRCenTX)
 ||     34: axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> axxu81(axxand(axxisNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ))),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     35: axxtail(cons(PeRCenTX,PeRCenTY)) -> axxu91(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY)
 ||     36: axxtake(PeRCenTX,PeRCenTY) -> axxu101(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||     37: mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu101(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     38: mark(fst(PeRCenTX)) -> axxfst(mark(PeRCenTX))
 ||     39: mark(splitAt(PeRCenTX,PeRCenTY)) -> axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||     40: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     41: mark(snd(PeRCenTX)) -> axxsnd(mark(PeRCenTX))
 ||     42: mark(u21(PeRCenTX,PeRCenTY)) -> axxu21(mark(PeRCenTX),PeRCenTY)
 ||     43: mark(u31(PeRCenTX,PeRCenTY)) -> axxu31(mark(PeRCenTX),PeRCenTY)
 ||     44: mark(u41(PeRCenTX,PeRCenTY)) -> axxu41(mark(PeRCenTX),PeRCenTY)
 ||     45: mark(natsFrom(PeRCenTX)) -> axxnatsFrom(mark(PeRCenTX))
 ||     46: mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu51(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||     47: mark(head(PeRCenTX)) -> axxhead(mark(PeRCenTX))
 ||     48: mark(afterNth(PeRCenTX,PeRCenTY)) -> axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||     49: mark(u61(PeRCenTX,PeRCenTY)) -> axxu61(mark(PeRCenTX),PeRCenTY)
 ||     50: mark(u71(PeRCenTX,PeRCenTY)) -> axxu71(mark(PeRCenTX),PeRCenTY)
 ||     51: mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     52: mark(u82(PeRCenTX,PeRCenTY)) -> axxu82(mark(PeRCenTX),PeRCenTY)
 ||     53: mark(u91(PeRCenTX,PeRCenTY)) -> axxu91(mark(PeRCenTX),PeRCenTY)
 ||     54: mark(and(PeRCenTX,PeRCenTY)) -> axxand(mark(PeRCenTX),PeRCenTY)
 ||     55: mark(isNatural(PeRCenTX)) -> axxisNatural(PeRCenTX)
 ||     56: mark(isLNat(PeRCenTX)) -> axxisLNat(PeRCenTX)
 ||     57: mark(isPLNat(PeRCenTX)) -> axxisPLNat(PeRCenTX)
 ||     58: mark(tail(PeRCenTX)) -> axxtail(mark(PeRCenTX))
 ||     59: mark(take(PeRCenTX,PeRCenTY)) -> axxtake(mark(PeRCenTX),mark(PeRCenTY))
 ||     60: mark(sel(PeRCenTX,PeRCenTY)) -> axxsel(mark(PeRCenTX),mark(PeRCenTY))
 ||     61: mark(tt()) -> tt()
 ||     62: mark(cons(PeRCenTX,PeRCenTY)) -> cons(mark(PeRCenTX),PeRCenTY)
 ||     63: mark(s(PeRCenTX)) -> s(mark(PeRCenTX))
 ||     64: mark(pair(PeRCenTX,PeRCenTY)) -> pair(mark(PeRCenTX),mark(PeRCenTY))
 ||     65: mark(nil()) -> nil()
 ||     66: mark(0()) -> 0()
 ||     67: axxu101(PeRCenTX,PeRCenTY,PeRCenTZ) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     68: axxfst(PeRCenTX) -> fst(PeRCenTX)
 ||     69: axxsplitAt(PeRCenTX,PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     70: axxu11(PeRCenTX,PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     71: axxsnd(PeRCenTX) -> snd(PeRCenTX)
 ||     72: axxu21(PeRCenTX,PeRCenTY) -> u21(PeRCenTX,PeRCenTY)
 ||     73: axxu31(PeRCenTX,PeRCenTY) -> u31(PeRCenTX,PeRCenTY)
 ||     74: axxu41(PeRCenTX,PeRCenTY) -> u41(PeRCenTX,PeRCenTY)
 ||     75: axxnatsFrom(PeRCenTX) -> natsFrom(PeRCenTX)
 ||     76: axxu51(PeRCenTX,PeRCenTY,PeRCenTZ) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     77: axxhead(PeRCenTX) -> head(PeRCenTX)
 ||     78: axxafterNth(PeRCenTX,PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     79: axxu61(PeRCenTX,PeRCenTY) -> u61(PeRCenTX,PeRCenTY)
 ||     80: axxu71(PeRCenTX,PeRCenTY) -> u71(PeRCenTX,PeRCenTY)
 ||     81: axxu81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     82: axxu82(PeRCenTX,PeRCenTY) -> u82(PeRCenTX,PeRCenTY)
 ||     83: axxu91(PeRCenTX,PeRCenTY) -> u91(PeRCenTX,PeRCenTY)
 ||     84: axxand(PeRCenTX,PeRCenTY) -> and(PeRCenTX,PeRCenTY)
 ||     85: axxisNatural(PeRCenTX) -> isNatural(PeRCenTX)
 ||     86: axxisLNat(PeRCenTX) -> isLNat(PeRCenTX)
 ||     87: axxisPLNat(PeRCenTX) -> isPLNat(PeRCenTX)
 ||     88: axxtail(PeRCenTX) -> tail(PeRCenTX)
 ||     89: axxtake(PeRCenTX,PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     90: axxsel(PeRCenTX,PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     91: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX
 ||     92: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY
 || Number of strict rules: 92
 || Direct POLO(bPol) ... failed.
 || Uncurrying ... failed.
 || Dependency Pairs:
 ||    #1: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #2: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #3: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #4: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #5: #mark(u31(PeRCenTX,PeRCenTY)) -> #axxu31(mark(PeRCenTX),PeRCenTY)
 ||    #6: #mark(u31(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #7: #axxisPLNat(splitAt(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #8: #axxisPLNat(splitAt(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 ||    #9: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #axxu91(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY)
 ||    #10: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #11: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 ||    #12: #mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu51(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #13: #mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #14: #mark(u21(PeRCenTX,PeRCenTY)) -> #axxu21(mark(PeRCenTX),PeRCenTY)
 ||    #15: #mark(u21(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #16: #mark(snd(PeRCenTX)) -> #axxsnd(mark(PeRCenTX))
 ||    #17: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #18: #mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu101(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #19: #mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #20: #mark(head(PeRCenTX)) -> #axxhead(mark(PeRCenTX))
 ||    #21: #mark(head(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #22: #mark(u91(PeRCenTX,PeRCenTY)) -> #axxu91(mark(PeRCenTX),PeRCenTY)
 ||    #23: #mark(u91(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #24: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #25: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #26: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #27: #mark(tail(PeRCenTX)) -> #axxtail(mark(PeRCenTX))
 ||    #28: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #29: #mark(fst(PeRCenTX)) -> #axxfst(mark(PeRCenTX))
 ||    #30: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #31: #axxu51(tt(),PeRCenTX,PeRCenTY) -> #axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #32: #axxu51(tt(),PeRCenTX,PeRCenTY) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #33: #axxu51(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #34: #axxu51(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #35: #mark(take(PeRCenTX,PeRCenTY)) -> #axxtake(mark(PeRCenTX),mark(PeRCenTY))
 ||    #36: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #37: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #38: #mark(isNatural(PeRCenTX)) -> #axxisNatural(PeRCenTX)
 ||    #39: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #40: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #41: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #42: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #43: #axxand(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #44: #axxu81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu82(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY)
 ||    #45: #axxu81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ))
 ||    #46: #axxu81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTX)
 ||    #47: #axxu81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTZ)
 ||    #48: #axxu91(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #49: #mark(isPLNat(PeRCenTX)) -> #axxisPLNat(PeRCenTX)
 ||    #50: #axxisLNat(take(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #51: #axxisLNat(take(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 ||    #52: #mark(natsFrom(PeRCenTX)) -> #axxnatsFrom(mark(PeRCenTX))
 ||    #53: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #54: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxu11(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||    #55: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #56: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxisNatural(PeRCenTX)
 ||    #57: #axxsel(PeRCenTX,PeRCenTY) -> #axxu51(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||    #58: #axxsel(PeRCenTX,PeRCenTY) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #59: #axxsel(PeRCenTX,PeRCenTY) -> #axxisNatural(PeRCenTX)
 ||    #60: #mark(isLNat(PeRCenTX)) -> #axxisLNat(PeRCenTX)
 ||    #61: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #axxu21(axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX)
 ||    #62: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY))
 ||    #63: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #axxisLNat(PeRCenTX)
 ||    #64: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #65: #axxnatsFrom(PeRCenTX) -> #axxu41(axxisNatural(PeRCenTX),PeRCenTX)
 ||    #66: #axxnatsFrom(PeRCenTX) -> #axxisNatural(PeRCenTX)
 ||    #67: #mark(u82(PeRCenTX,PeRCenTY)) -> #axxu82(mark(PeRCenTX),PeRCenTY)
 ||    #68: #mark(u82(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #69: #mark(u61(PeRCenTX,PeRCenTY)) -> #axxu61(mark(PeRCenTX),PeRCenTY)
 ||    #70: #mark(u61(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #71: #axxisNatural(head(PeRCenTX)) -> #axxisLNat(PeRCenTX)
 ||    #72: #axxisLNat(natsFrom(PeRCenTX)) -> #axxisNatural(PeRCenTX)
 ||    #73: #axxu61(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #74: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #75: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #76: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #77: #axxu82(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTZ)
 ||    #78: #axxu82(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTY)
 ||    #79: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #80: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #81: #axxsplitAt(0(),PeRCenTX) -> #axxu71(axxisLNat(PeRCenTX),PeRCenTX)
 ||    #82: #axxsplitAt(0(),PeRCenTX) -> #axxisLNat(PeRCenTX)
 ||    #83: #axxu41(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #84: #mark(u41(PeRCenTX,PeRCenTY)) -> #axxu41(mark(PeRCenTX),PeRCenTY)
 ||    #85: #mark(u41(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #86: #axxisPLNat(pair(PeRCenTX,PeRCenTY)) -> #axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY))
 ||    #87: #axxisPLNat(pair(PeRCenTX,PeRCenTY)) -> #axxisLNat(PeRCenTX)
 ||    #88: #axxisLNat(tail(PeRCenTX)) -> #axxisLNat(PeRCenTX)
 ||    #89: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxu81(axxand(axxisNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ))),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #90: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxand(axxisNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ)))
 ||    #91: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxisNatural(PeRCenTX)
 ||    #92: #axxisNatural(sel(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #93: #axxisNatural(sel(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 ||    #94: #mark(sel(PeRCenTX,PeRCenTY)) -> #axxsel(mark(PeRCenTX),mark(PeRCenTY))
 ||    #95: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #96: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #97: #axxisLNat(afterNth(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #98: #axxisLNat(afterNth(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 ||    #99: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #axxu61(axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY)
 ||    #100: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #axxand(axxisLNat(PeRCenTX),isLNat(PeRCenTY))
 ||    #101: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #axxisLNat(PeRCenTX)
 ||    #102: #axxisLNat(fst(PeRCenTX)) -> #axxisPLNat(PeRCenTX)
 ||    #103: #mark(s(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #104: #axxisNatural(s(PeRCenTX)) -> #axxisNatural(PeRCenTX)
 ||    #105: #axxtake(PeRCenTX,PeRCenTY) -> #axxu101(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||    #106: #axxtake(PeRCenTX,PeRCenTY) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #107: #axxtake(PeRCenTX,PeRCenTY) -> #axxisNatural(PeRCenTX)
 ||    #108: #axxisLNat(snd(PeRCenTX)) -> #axxisPLNat(PeRCenTX)
 ||    #109: #axxu21(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #110: #axxu101(tt(),PeRCenTX,PeRCenTY) -> #axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #111: #axxu101(tt(),PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #112: #axxu101(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX)
 ||    #113: #axxu101(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY)
 ||    #114: #mark(and(PeRCenTX,PeRCenTY)) -> #axxand(mark(PeRCenTX),PeRCenTY)
 ||    #115: #mark(and(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #116: #axxu71(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #117: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #axxu31(axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX)
 ||    #118: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #119: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 ||    #120: #axxu31(tt(),PeRCenTX) -> #mark(PeRCenTX)
 ||    #121: #mark(u71(PeRCenTX,PeRCenTY)) -> #axxu71(mark(PeRCenTX),PeRCenTY)
 ||    #122: #mark(u71(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #123: #axxisLNat(cons(PeRCenTX,PeRCenTY)) -> #axxand(axxisNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #124: #axxisLNat(cons(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX)
 || Number of SCCs: 1, DPs: 124
 ||   SCC { #1..124 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1, x2 + 5, x3 + 7, x4 + 10)
 ||       #axxu51	w: max(x2 + 26, x3 + 26)
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1
 ||       axxisLNat	w: x1
 ||       u91	w: max(x1, x2)
 ||       #axxu82	w: max(x1, x2)
 ||       isPLNat	w: x1 + 1
 ||       axxsnd	w: x1 + 12
 ||       axxu11	w: max(x1 + 12, x2 + 23, x3 + 22)
 ||       #axxu101	w: max(x2 + 11, x3 + 13)
 ||       #axxisLNat	w: x1
 ||       take	w: max(x1 + 15, x2 + 14)
 ||       and	w: max(x1, x2)
 ||       axxsplitAt	w: max(x1 + 5, x2 + 10)
 ||       pair	w: max(x1 + 7, x2 + 8)
 ||       axxu91	w: max(x1, x2)
 ||       fst	w: x1 + 1
 ||       axxand	w: max(x1, x2)
 ||       natsFrom	w: x1
 ||       splitAt	w: max(x1 + 5, x2 + 10)
 ||       #axxu11	w: max(x1 + 7, x2 + 11, x3 + 11)
 ||       u61	w: max(x1 + 8, x2 + 7)
 ||       axxu31	w: max(x1 + 2, x2 + 3)
 ||       isNatural	w: x1
 ||       #axxsplitAt	w: max(x1 + 5, x2 + 10)
 ||       axxnatsFrom	w: x1
 ||       u41	w: max(x1, x2)
 ||       axxisNatural	w: x1
 ||       #axxu91	w: max(x1, x2)
 ||       tail	w: x1
 ||       u51	w: max(x1 + 29, x2 + 28, x3 + 27)
 ||       #axxafterNth	w: max(x1 + 12, x2 + 12)
 ||       #mark	w: x1
 ||       #axxtail	w: x1
 ||       0 	w: 4
 ||       axxu82	w: max(x1, x2 + 7)
 ||       #axxnatsFrom	w: x1
 ||       axxu81	w: max(x1, x2 + 5, x3 + 7, x4 + 10)
 ||       axxisPLNat	w: x1 + 1
 ||       #axxisPLNat	w: x1
 ||       u11	w: max(x1 + 12, x2 + 23, x3 + 22)
 ||       sel	w: max(x1 + 29, x2 + 30)
 ||       afterNth	w: max(x1 + 23, x2 + 22)
 ||       nil	w: 4
 ||       #axxsnd	w: x1
 ||       isLNat	w: x1
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: max(x2 + 1)
 ||       axxu41	w: max(x1, x2)
 ||       axxafterNth	w: max(x1 + 23, x2 + 22)
 ||       mark	w: x1
 ||       axxu71	w: max(x1 + 7, x2 + 10)
 ||       u101	w: max(x1, x2 + 15, x3 + 14)
 ||       #axxu81	w: max(x2 + 5, x3, x4 + 10)
 ||       axxsel	w: max(x1 + 29, x2 + 30)
 ||       u21	w: max(x1, x2 + 2)
 ||       axxfst	w: x1 + 1
 ||       axxu61	w: max(x1 + 8, x2 + 7)
 ||       u82	w: max(x1, x2 + 7)
 ||       #axxu31	w: max(x2 + 1)
 ||       #axxand	w: max(x2)
 ||       #axxsel	w: max(x1 + 27, x2 + 27)
 ||       axxu51	w: max(x1 + 29, x2 + 28, x3 + 27)
 ||       head	w: x1 + 5
 ||       cons	w: max(x1, x2)
 ||       snd	w: x1 + 12
 ||       #axxu41	w: max(x2)
 ||       axxtail	w: x1
 ||       tt	w: 4
 ||       u71	w: max(x1 + 7, x2 + 10)
 ||       axxtake	w: max(x1 + 15, x2 + 14)
 ||       #axxu61	w: max(x2 + 2)
 ||       #axxfst	w: x1
 ||       axxu101	w: max(x1, x2 + 15, x3 + 14)
 ||       #axxu71	w: max(x2 + 8)
 ||       #axxisNatural	w: x1
 ||       u31	w: max(x1 + 2, x2 + 3)
 ||       axxu21	w: max(x1, x2 + 2)
 ||       #axxtake	w: max(x1 + 12, x2 + 13)
 ||       #axxhead	w: x1 + 2
 ||       axxhead	w: x1 + 5
 ||     USABLE RULES: { 1..90 }
 ||     Removed DPs: #1..8 #12..14 #16..18 #20 #21 #24..26 #29..37 #39 #40 #46 #47 #49..51 #54..59 #61..63 #69..71 #73 #75 #76 #78..82 #86 #87 #90..102 #106..113 #116..122
 || Number of SCCs: 2, DPs: 33
 ||   SCC { #104 }
 || POLO(Sum)... succeeded.
 ||       u81	w: x1 + x3 + 1
 ||       #axxu51	w: 1
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1 + 1
 ||       axxisLNat	w: x1 + 13
 ||       u91	w: 1
 ||       #axxu82	w: 1
 ||       isPLNat	w: 1
 ||       axxsnd	w: 3
 ||       axxu11	w: x2 + 2
 ||       #axxu101	w: 1
 ||       #axxisLNat	w: 1
 ||       take	w: x2 + 1
 ||       and	w: x1 + x2 + 8
 ||       axxsplitAt	w: 11
 ||       pair	w: x1 + x2 + 1
 ||       axxu91	w: 11
 ||       fst	w: x1 + 5
 ||       axxand	w: x1 + 7
 ||       natsFrom	w: 1
 ||       splitAt	w: x1 + x2 + 1
 ||       #axxu11	w: 1
 ||       u61	w: x2 + 1
 ||       axxu31	w: 11
 ||       isNatural	w: 1
 ||       #axxsplitAt	w: 1
 ||       axxnatsFrom	w: x1 + 11
 ||       u41	w: 1
 ||       axxisNatural	w: x1 + 11
 ||       #axxu91	w: 1
 ||       tail	w: x1 + 12
 ||       u51	w: x1 + x2 + x3 + 13
 ||       #axxafterNth	w: 1
 ||       #mark	w: 1
 ||       #axxtail	w: 1
 ||       0 	w: 1
 ||       axxu82	w: 0
 ||       #axxnatsFrom	w: 1
 ||       axxu81	w: x1 + x4 + 2
 ||       axxisPLNat	w: x1 + 18
 ||       #axxisPLNat	w: 1
 ||       u11	w: x3 + 3
 ||       sel	w: 1
 ||       afterNth	w: x1 + 1
 ||       nil	w: 3
 ||       #axxsnd	w: 1
 ||       isLNat	w: 1
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: 1
 ||       axxu41	w: 11
 ||       axxafterNth	w: x1 + x2 + 1
 ||       mark	w: x1 + 9
 ||       axxu71	w: 12
 ||       u101	w: x2 + x3 + 2
 ||       #axxu81	w: 1
 ||       axxsel	w: 11
 ||       u21	w: x1 + x2 + 1
 ||       axxfst	w: 15
 ||       axxu61	w: x2 + 11
 ||       u82	w: 1
 ||       #axxu31	w: 1
 ||       #axxand	w: 1
 ||       #axxsel	w: 1
 ||       axxu51	w: x2 + 12
 ||       head	w: 1
 ||       cons	w: 1
 ||       snd	w: 4
 ||       #axxu41	w: 1
 ||       axxtail	w: 11
 ||       tt	w: 1
 ||       u71	w: x1 + x2 + 13
 ||       axxtake	w: x2
 ||       #axxu61	w: 1
 ||       #axxfst	w: 1
 ||       axxu101	w: 1
 ||       #axxu71	w: 1
 ||       #axxisNatural	w: x1 + 1
 ||       u31	w: x1 + x2 + 1
 ||       axxu21	w: x1
 ||       #axxtake	w: 1
 ||       #axxhead	w: 0
 ||       axxhead	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #104
 || Number of SCCs: 1, DPs: 32
 ||   SCC { #9 #10 #15 #19 #22 #23 #27 #28 #41..45 #48 #52 #53 #60 #64 #65 #67 #68 #74 #77 #83..85 #88 #89 #103 #114 #115 #123 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1, x2 + 5, x3 + 7, x4 + 10)
 ||       #axxu51	w: 0
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1
 ||       axxisLNat	w: x1
 ||       u91	w: max(x1, x2)
 ||       #axxu82	w: max(x1 + 1, x2 + 11)
 ||       isPLNat	w: x1 + 1
 ||       axxsnd	w: x1 + 12
 ||       axxu11	w: max(x1 + 12, x2 + 23, x3 + 22)
 ||       #axxu101	w: 0
 ||       #axxisLNat	w: x1 + 10
 ||       take	w: max(x1 + 15, x2 + 14)
 ||       and	w: max(x1, x2)
 ||       axxsplitAt	w: max(x1 + 5, x2 + 10)
 ||       pair	w: max(x1 + 7, x2 + 8)
 ||       axxu91	w: max(x1, x2)
 ||       fst	w: x1 + 1
 ||       axxand	w: max(x1, x2)
 ||       natsFrom	w: x1
 ||       splitAt	w: max(x1 + 5, x2 + 10)
 ||       #axxu11	w: max(x1 + 7)
 ||       u61	w: max(x1 + 8, x2 + 7)
 ||       axxu31	w: max(x1 + 2, x2 + 3)
 ||       isNatural	w: x1
 ||       #axxsplitAt	w: max(x1 + 13, x2 + 12)
 ||       axxnatsFrom	w: x1
 ||       u41	w: max(x1, x2)
 ||       axxisNatural	w: x1
 ||       #axxu91	w: max(x1 + 1, x2 + 10)
 ||       tail	w: x1 + 2
 ||       u51	w: max(x1 + 29, x2 + 28, x3 + 27)
 ||       #axxafterNth	w: max(x1 + 12, x2 + 12)
 ||       #mark	w: x1 + 10
 ||       #axxtail	w: x1 + 11
 ||       0 	w: 4
 ||       axxu82	w: max(x1, x2 + 7)
 ||       #axxnatsFrom	w: x1 + 10
 ||       axxu81	w: max(x1, x2 + 5, x3 + 7, x4 + 10)
 ||       axxisPLNat	w: x1 + 1
 ||       #axxisPLNat	w: 0
 ||       u11	w: max(x1 + 12, x2 + 23, x3 + 22)
 ||       sel	w: max(x1 + 29, x2 + 30)
 ||       afterNth	w: max(x1 + 23, x2 + 22)
 ||       nil	w: 4
 ||       #axxsnd	w: x1
 ||       isLNat	w: x1
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: 0
 ||       axxu41	w: max(x1, x2)
 ||       axxafterNth	w: max(x1 + 23, x2 + 22)
 ||       mark	w: x1
 ||       axxu71	w: max(x1 + 7, x2 + 10)
 ||       u101	w: max(x1, x2 + 15, x3 + 14)
 ||       #axxu81	w: max(x2 + 13, x3 + 12, x4 + 12)
 ||       axxsel	w: max(x1 + 29, x2 + 30)
 ||       u21	w: max(x1, x2 + 2)
 ||       axxfst	w: x1 + 1
 ||       axxu61	w: max(x1 + 8, x2 + 7)
 ||       u82	w: max(x1, x2 + 7)
 ||       #axxu31	w: 0
 ||       #axxand	w: max(x2 + 10)
 ||       #axxsel	w: max(x1 + 27, x2 + 27)
 ||       axxu51	w: max(x1 + 29, x2 + 28, x3 + 27)
 ||       head	w: x1 + 5
 ||       cons	w: max(x1, x2)
 ||       snd	w: x1 + 12
 ||       #axxu41	w: max(x1 + 7, x2 + 10)
 ||       axxtail	w: x1 + 2
 ||       tt	w: 4
 ||       u71	w: max(x1 + 7, x2 + 10)
 ||       axxtake	w: max(x1 + 15, x2 + 14)
 ||       #axxu61	w: 0
 ||       #axxfst	w: x1
 ||       axxu101	w: max(x1, x2 + 15, x3 + 14)
 ||       #axxu71	w: 0
 ||       #axxisNatural	w: 0
 ||       u31	w: max(x1 + 2, x2 + 3)
 ||       axxu21	w: max(x1, x2 + 2)
 ||       #axxtake	w: max(x1 + 12, x2 + 13)
 ||       #axxhead	w: x1 + 2
 ||       axxhead	w: x1 + 5
 ||     USABLE RULES: { 1..90 }
 ||     Removed DPs: #9 #10 #27 #28 #41 #44 #67 #74 #77 #88
 || Number of SCCs: 2, DPs: 22
 ||   SCC { #45 #89 }
 || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded.
 ||       u81	s: []	p: 6	w: max(x3 + 9, x4 + 11)
 ||       #axxu51	s: []	p: 0	w: x2
 ||       TIlDePAIR	s: []	p: 0	w: x2 + 1
 ||       s 	s: [1]	p: 4	w: x1
 ||       axxisLNat	s: []	p: 1	w: x1 + 1
 ||       u91	s: []	p: 3	w: max(x1 + 2, x2 + 1)
 ||       #axxu82	s: [1]	p: 0	w: x1 + 1
 ||       isPLNat	s: 1
 ||       axxsnd	s: []	p: 8	w: x1 + 5
 ||       axxu11	s: []	p: 7	w: max(x1 + 17, x3 + 17)
 ||       #axxu101	s: []	p: 0	w: max(x1 + 1)
 ||       #axxisLNat	s: []	p: 0	w: 1
 ||       take	s: []	p: 6	w: x1 + x2 + 17
 ||       and	s: 2
 ||       axxsplitAt	s: []	p: 6	w: max(x2 + 11)
 ||       pair	s: []	p: 4	w: max(x1 + 2, x2 + 9)
 ||       axxu91	s: []	p: 3	w: max(x1 + 2, x2 + 1)
 ||       fst	s: []	p: 0	w: x1 + 4
 ||       axxand	s: 2
 ||       natsFrom	s: []	p: 3	w: x1 + 2
 ||       splitAt	s: []	p: 6	w: max(x2 + 11)
 ||       #axxu11	s: [3]	p: 0	w: x3
 ||       u61	s: []	p: 9	w: max(x2 + 8)
 ||       axxu31	s: 2
 ||       isNatural	s: []	p: 2	w: x1
 ||       #axxsplitAt	s: 1
 ||       axxnatsFrom	s: []	p: 3	w: x1 + 2
 ||       u41	s: []	p: 3	w: max(x1 + 1, x2 + 2)
 ||       axxisNatural	s: []	p: 2	w: x1
 ||       #axxu91	s: [1,2]	p: 0	w: max(x1 + 1, x2)
 ||       tail	s: []	p: 3	w: x1 + 4
 ||       u51	s: []	p: 3	w: max(x1 + 18, x3 + 22)
 ||       #axxafterNth	s: [1,2]	p: 0	w: x1 + x2
 ||       #mark	s: []	p: 0	w: 0
 ||       #axxtail	s: []	p: 0	w: 0
 ||       0 	s: []	p: 4	w: 4
 ||       axxu82	s: []	p: 4	w: max(x1, x2 + 3)
 ||       #axxnatsFrom	s: []	p: 0	w: 0
 ||       axxu81	s: []	p: 6	w: max(x3 + 9, x4 + 11)
 ||       axxisPLNat	s: 1
 ||       #axxisPLNat	s: []	p: 0	w: 0
 ||       u11	s: []	p: 7	w: max(x1 + 17, x3 + 17)
 ||       sel	s: []	p: 3	w: x2 + 23
 ||       afterNth	s: []	p: 8	w: max(x2 + 19)
 ||       nil	s: []	p: 4	w: 3
 ||       #axxsnd	s: []	p: 0	w: 0
 ||       isLNat	s: []	p: 1	w: x1 + 1
 ||       #TIlDePAIR	s: []	p: 0	w: 1
 ||       #axxu21	s: []	p: 0	w: x1
 ||       axxu41	s: []	p: 3	w: max(x1 + 1, x2 + 2)
 ||       axxafterNth	s: []	p: 8	w: max(x2 + 19)
 ||       mark	s: 1
 ||       axxu71	s: []	p: 5	w: max(x1, x2 + 10)
 ||       u101	s: []	p: 6	w: max(x2, x3 + 16)
 ||       #axxu81	s: [2]	p: 4	w: max(x2)
 ||       axxsel	s: []	p: 3	w: x2 + 23
 ||       u21	s: [1]	p: 4	w: max(x1, x2 + 5)
 ||       axxfst	s: []	p: 0	w: x1 + 4
 ||       axxu61	s: []	p: 9	w: max(x2 + 8)
 ||       u82	s: []	p: 4	w: max(x1, x2 + 3)
 ||       #axxu31	s: []	p: 0	w: x1 + 1
 ||       #axxand	s: [1,2]	p: 0	w: max(x1, x2 + 1)
 ||       #axxsel	s: []	p: 0	w: x2 + 1
 ||       axxu51	s: []	p: 3	w: max(x1 + 18, x3 + 22)
 ||       head	s: []	p: 3	w: x1 + 2
 ||       cons	s: []	p: 1	w: max(x1, x2)
 ||       snd	s: []	p: 8	w: x1 + 5
 ||       #axxu41	s: [1,2]	p: 0	w: max(x1 + 1, x2 + 1)
 ||       axxtail	s: []	p: 3	w: x1 + 4
 ||       tt	s: []	p: 1	w: 4
 ||       u71	s: []	p: 5	w: max(x1, x2 + 10)
 ||       axxtake	s: []	p: 6	w: x1 + x2 + 17
 ||       #axxu61	s: []	p: 0	w: x1
 ||       #axxfst	s: []	p: 0	w: 0
 ||       axxu101	s: []	p: 6	w: max(x2, x3 + 16)
 ||       #axxu71	s: []	p: 0	w: x1 + 1
 ||       #axxisNatural	s: []	p: 0	w: 0
 ||       u31	s: 2
 ||       axxu21	s: [1]	p: 4	w: max(x1, x2 + 5)
 ||       #axxtake	s: []	p: 0	w: x1
 ||       #axxhead	s: []	p: 0	w: 0
 ||       axxhead	s: []	p: 3	w: x1 + 2
 ||     USABLE RULES: { 1..90 }
 ||     Removed DPs: #45
 || Number of SCCs: 1, DPs: 20
 ||   SCC { #15 #19 #22 #23 #42 #43 #48 #52 #53 #60 #64 #65 #68 #83..85 #103 #114 #115 #123 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1 + 1, x2 + 4, x3 + 5, x4 + 6)
 ||       #axxu51	w: 0
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1
 ||       axxisLNat	w: x1 + 3
 ||       u91	w: max(x1 + 1, x2 + 3)
 ||       #axxu82	w: 0
 ||       isPLNat	w: x1 + 6
 ||       axxsnd	w: x1 + 6
 ||       axxu11	w: max(x1 + 4, x2 + 10, x3 + 12)
 ||       #axxu101	w: 0
 ||       #axxisLNat	w: x1 + 3
 ||       take	w: max(x1 + 10, x2 + 9)
 ||       and	w: max(x1 + 1, x2)
 ||       axxsplitAt	w: max(x1 + 4, x2 + 6)
 ||       pair	w: max(x1 + 3, x2 + 6)
 ||       axxu91	w: max(x1 + 1, x2 + 3)
 ||       fst	w: x1 + 3
 ||       axxand	w: max(x1 + 1, x2)
 ||       natsFrom	w: x1 + 8
 ||       splitAt	w: max(x1 + 4, x2 + 6)
 ||       #axxu11	w: 0
 ||       u61	w: max(x1 + 2, x2 + 1)
 ||       axxu31	w: max(x1 + 1, x2)
 ||       isNatural	w: x1 + 1
 ||       #axxsplitAt	w: 0
 ||       axxnatsFrom	w: x1 + 8
 ||       u41	w: max(x1 + 2, x2 + 8)
 ||       axxisNatural	w: x1 + 1
 ||       #axxu91	w: max(x2 + 2)
 ||       tail	w: x1 + 4
 ||       u51	w: max(x1 + 15, x2 + 17, x3 + 16)
 ||       #axxafterNth	w: 0
 ||       #mark	w: x1
 ||       #axxtail	w: 11
 ||       0 	w: 4
 ||       axxu82	w: max(x1, x2 + 5)
 ||       #axxnatsFrom	w: x1 + 3
 ||       axxu81	w: max(x1 + 1, x2 + 4, x3 + 5, x4 + 6)
 ||       axxisPLNat	w: x1 + 6
 ||       #axxisPLNat	w: 0
 ||       u11	w: max(x1 + 4, x2 + 10, x3 + 12)
 ||       sel	w: max(x1 + 17, x2 + 30)
 ||       afterNth	w: max(x1 + 13, x2 + 12)
 ||       nil	w: 4
 ||       #axxsnd	w: 0
 ||       isLNat	w: x1 + 3
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: 0
 ||       axxu41	w: max(x1 + 2, x2 + 8)
 ||       axxafterNth	w: max(x1 + 13, x2 + 12)
 ||       mark	w: x1
 ||       axxu71	w: max(x1 + 3, x2 + 6)
 ||       u101	w: max(x1 + 1, x2 + 10, x3 + 9)
 ||       #axxu81	w: 0
 ||       axxsel	w: max(x1 + 17, x2 + 30)
 ||       u21	w: max(x1 + 1, x2 + 2)
 ||       axxfst	w: x1 + 3
 ||       axxu61	w: max(x1 + 2, x2 + 1)
 ||       u82	w: max(x1, x2 + 5)
 ||       #axxu31	w: 0
 ||       #axxand	w: max(x2)
 ||       #axxsel	w: 0
 ||       axxu51	w: max(x1 + 15, x2 + 17, x3 + 16)
 ||       head	w: x1 + 4
 ||       cons	w: max(x1, x2)
 ||       snd	w: x1 + 6
 ||       #axxu41	w: max(x1 + 1, x2)
 ||       axxtail	w: x1 + 4
 ||       tt	w: 5
 ||       u71	w: max(x1 + 3, x2 + 6)
 ||       axxtake	w: max(x1 + 10, x2 + 9)
 ||       #axxu61	w: 0
 ||       #axxfst	w: 0
 ||       axxu101	w: max(x1 + 1, x2 + 10, x3 + 9)
 ||       #axxu71	w: 0
 ||       #axxisNatural	w: 0
 ||       u31	w: max(x1 + 1, x2)
 ||       axxu21	w: max(x1 + 1, x2 + 2)
 ||       #axxtake	w: 0
 ||       #axxhead	w: 2
 ||       axxhead	w: x1 + 4
 ||     USABLE RULES: { 1..90 }
 ||     Removed DPs: #15 #19 #22 #23 #42 #48 #52 #53 #65 #84 #85 #115
 || Number of SCCs: 1, DPs: 7
 ||   SCC { #43 #60 #64 #68 #103 #114 #123 }
 || POLO(Sum)... succeeded.
 ||       u81	w: x3 + x4 + 5
 ||       #axxu51	w: 1
 ||       TIlDePAIR	w: 0
 ||       s 	w: x1 + 1
 ||       axxisLNat	w: x1 + 7
 ||       u91	w: 1
 ||       #axxu82	w: 1
 ||       isPLNat	w: x1 + 6
 ||       axxsnd	w: 3
 ||       axxu11	w: x3 + 2
 ||       #axxu101	w: 1
 ||       #axxisLNat	w: x1 + 2
 ||       take	w: x1 + 4
 ||       and	w: x2 + 3
 ||       axxsplitAt	w: 7
 ||       pair	w: 9
 ||       axxu91	w: 1
 ||       fst	w: x1 + 5
 ||       axxand	w: 2
 ||       natsFrom	w: 1
 ||       splitAt	w: 1
 ||       #axxu11	w: 1
 ||       u61	w: x1 + x2 + 5
 ||       axxu31	w: 1
 ||       isNatural	w: x1 + 2
 ||       #axxsplitAt	w: 0
 ||       axxnatsFrom	w: 3
 ||       u41	w: x1 + x2 + 4
 ||       axxisNatural	w: 1
 ||       #axxu91	w: 3
 ||       tail	w: 1
 ||       u51	w: x1 + x2 + 2
 ||       #axxafterNth	w: 1
 ||       #mark	w: x1 + 2
 ||       #axxtail	w: 2
 ||       0 	w: 1
 ||       axxu82	w: 16
 ||       #axxnatsFrom	w: 2
 ||       axxu81	w: x1 + x2 + x3 + x4 + 6
 ||       axxisPLNat	w: 12
 ||       #axxisPLNat	w: 1
 ||       u11	w: x1 + 3
 ||       sel	w: 1
 ||       afterNth	w: x2 + 2
 ||       nil	w: 1
 ||       #axxsnd	w: 1
 ||       isLNat	w: x1 + 1
 ||       #TIlDePAIR	w: 0
 ||       #axxu21	w: 1
 ||       axxu41	w: 3
 ||       axxafterNth	w: 1
 ||       mark	w: x1 + 5
 ||       axxu71	w: 8
 ||       u101	w: x2 + x3 + 12
 ||       #axxu81	w: 0
 ||       axxsel	w: x1 + x2
 ||       u21	w: x2 + 1
 ||       axxfst	w: 11
 ||       axxu61	w: 4
 ||       u82	w: x1 + x2 + 17
 ||       #axxu31	w: 1
 ||       #axxand	w: x2 + 3
 ||       #axxsel	w: 1
 ||       axxu51	w: x3 + 1
 ||       head	w: 3
 ||       cons	w: x1 + x2 + 3
 ||       snd	w: 4
 ||       #axxu41	w: 2
 ||       axxtail	w: x1 + 2
 ||       tt	w: 9
 ||       u71	w: x2 + 2
 ||       axxtake	w: x1 + 3
 ||       #axxu61	w: 1
 ||       #axxfst	w: 1
 ||       axxu101	w: x2 + 11
 ||       #axxu71	w: 1
 ||       #axxisNatural	w: 1
 ||       u31	w: x2 + 2
 ||       axxu21	w: 0
 ||       #axxtake	w: 1
 ||       #axxhead	w: 0
 ||       axxhead	w: 2
 ||     USABLE RULES: { }
 ||     Removed DPs: #43 #60 #64 #68 #103 #114 #123
 || 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:


  Rules R_0:

    axxu101(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) 
    axxu11(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) 
    axxu21(tt, X) => mark(X) 
    axxu31(tt, X) => mark(X) 
    axxu41(tt, X) => cons(mark(X), natsFrom(s(X))) 
    axxu51(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) 
    axxu61(tt, X) => mark(X) 
    axxu71(tt, X) => pair(nil, mark(X)) 
    axxu81(tt, X, Y, Z) => axxu82(axxsplitAt(mark(X), mark(Z)), Y) 
    axxu82(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) 
    axxu91(tt, X) => mark(X) 
    axxafterNth(X, Y) => axxu11(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    axxand(tt, X) => mark(X) 
    axxfst(pair(X, Y)) => axxu21(axxand(axxisLNat(X), isLNat(Y)), X) 
    axxhead(cons(X, Y)) => axxu31(axxand(axxisNatural(X), isLNat(Y)), X) 
    axxisLNat(nil) => tt 
    axxisLNat(afterNth(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisLNat(cons(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisLNat(fst(X)) => axxisPLNat(X) 
    axxisLNat(natsFrom(X)) => axxisNatural(X) 
    axxisLNat(snd(X)) => axxisPLNat(X) 
    axxisLNat(tail(X)) => axxisLNat(X) 
    axxisLNat(take(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisNatural(0) => tt 
    axxisNatural(head(X)) => axxisLNat(X) 
    axxisNatural(s(X)) => axxisNatural(X) 
    axxisNatural(sel(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxisPLNat(pair(X, Y)) => axxand(axxisLNat(X), isLNat(Y)) 
    axxisPLNat(splitAt(X, Y)) => axxand(axxisNatural(X), isLNat(Y)) 
    axxnatsFrom(X) => axxu41(axxisNatural(X), X) 
    axxsel(X, Y) => axxu51(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    axxsnd(pair(X, Y)) => axxu61(axxand(axxisLNat(X), isLNat(Y)), Y) 
    axxsplitAt(0, X) => axxu71(axxisLNat(X), X) 
    axxsplitAt(s(X), cons(Y, Z)) => axxu81(axxand(axxisNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z) 
    axxtail(cons(X, Y)) => axxu91(axxand(axxisNatural(X), isLNat(Y)), Y) 
    axxtake(X, Y) => axxu101(axxand(axxisNatural(X), isLNat(Y)), X, Y) 
    mark(u101(X, Y, Z)) => axxu101(mark(X), Y, Z) 
    mark(fst(X)) => axxfst(mark(X)) 
    mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) 
    mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) 
    mark(snd(X)) => axxsnd(mark(X)) 
    mark(u21(X, Y)) => axxu21(mark(X), Y) 
    mark(u31(X, Y)) => axxu31(mark(X), Y) 
    mark(u41(X, Y)) => axxu41(mark(X), Y) 
    mark(natsFrom(X)) => axxnatsFrom(mark(X)) 
    mark(u51(X, Y, Z)) => axxu51(mark(X), Y, Z) 
    mark(head(X)) => axxhead(mark(X)) 
    mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) 
    mark(u61(X, Y)) => axxu61(mark(X), Y) 
    mark(u71(X, Y)) => axxu71(mark(X), Y) 
    mark(u81(X, Y, Z, U)) => axxu81(mark(X), Y, Z, U) 
    mark(u82(X, Y)) => axxu82(mark(X), Y) 
    mark(u91(X, Y)) => axxu91(mark(X), Y) 
    mark(and(X, Y)) => axxand(mark(X), Y) 
    mark(isNatural(X)) => axxisNatural(X) 
    mark(isLNat(X)) => axxisLNat(X) 
    mark(isPLNat(X)) => axxisPLNat(X) 
    mark(tail(X)) => axxtail(mark(X)) 
    mark(take(X, Y)) => axxtake(mark(X), mark(Y)) 
    mark(sel(X, Y)) => axxsel(mark(X), mark(Y)) 
    mark(tt) => tt 
    mark(cons(X, Y)) => cons(mark(X), Y) 
    mark(s(X)) => s(mark(X)) 
    mark(pair(X, Y)) => pair(mark(X), mark(Y)) 
    mark(nil) => nil 
    mark(0) => 0 
    axxu101(X, Y, Z) => u101(X, Y, Z) 
    axxfst(X) => fst(X) 
    axxsplitAt(X, Y) => splitAt(X, Y) 
    axxu11(X, Y, Z) => u11(X, Y, Z) 
    axxsnd(X) => snd(X) 
    axxu21(X, Y) => u21(X, Y) 
    axxu31(X, Y) => u31(X, Y) 
    axxu41(X, Y) => u41(X, Y) 
    axxnatsFrom(X) => natsFrom(X) 
    axxu51(X, Y, Z) => u51(X, Y, Z) 
    axxhead(X) => head(X) 
    axxafterNth(X, Y) => afterNth(X, Y) 
    axxu61(X, Y) => u61(X, Y) 
    axxu71(X, Y) => u71(X, Y) 
    axxu81(X, Y, Z, U) => u81(X, Y, Z, U) 
    axxu82(X, Y) => u82(X, Y) 
    axxu91(X, Y) => u91(X, Y) 
    axxand(X, Y) => and(X, Y) 
    axxisNatural(X) => isNatural(X) 
    axxisLNat(X) => isLNat(X) 
    axxisPLNat(X) => isPLNat(X) 
    axxtail(X) => tail(X) 
    axxtake(X, Y) => take(X, Y) 
    axxsel(X, Y) => sel(X, Y) 
    map(/\x.X(x), nil) => nil 
    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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:


This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

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.