We consider the system h34. Alphabet: 0 : [] --> A afterNth : [] --> A -> A -> A app : [] --> (A -> A) -> A -> A axxafterNth : [] --> 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 axxu102 : [] --> A -> A axxu11 : [] --> A -> A -> A -> A axxu111 : [] --> A -> A axxu12 : [] --> A -> A -> A -> A axxu121 : [] --> A -> A axxu131 : [] --> A -> A -> A axxu132 : [] --> A -> A axxu141 : [] --> A -> A -> A axxu142 : [] --> A -> A axxu151 : [] --> A -> A -> A axxu152 : [] --> A -> A axxu161 : [] --> A -> A -> A axxu171 : [] --> A -> A -> A -> A axxu172 : [] --> A -> A -> A -> A axxu181 : [] --> A -> A -> A axxu182 : [] --> A -> A -> A axxu191 : [] --> A -> A -> A axxu201 : [] --> A -> A -> A -> A -> A axxu202 : [] --> A -> A -> A -> A -> A axxu203 : [] --> A -> A -> A -> A -> A axxu204 : [] --> A -> A -> A axxu21 : [] --> A -> A -> A -> A axxu211 : [] --> A -> A -> A axxu212 : [] --> A -> A -> A axxu22 : [] --> A -> A -> A axxu221 : [] --> A -> A -> A -> A axxu222 : [] --> A -> A -> A -> A axxu31 : [] --> A -> A -> A -> A axxu32 : [] --> A -> A -> A axxu41 : [] --> A -> A -> A axxu42 : [] --> A -> A axxu51 : [] --> A -> A -> A axxu52 : [] --> A -> A axxu61 : [] --> A -> A axxu71 : [] --> A -> A axxu81 : [] --> A -> A axxu91 : [] --> 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 u102 : [] --> A -> A u11 : [] --> A -> A -> A -> A u111 : [] --> A -> A u12 : [] --> A -> A -> A -> A u121 : [] --> A -> A u131 : [] --> A -> A -> A u132 : [] --> A -> A u141 : [] --> A -> A -> A u142 : [] --> A -> A u151 : [] --> A -> A -> A u152 : [] --> A -> A u161 : [] --> A -> A -> A u171 : [] --> A -> A -> A -> A u172 : [] --> A -> A -> A -> A u181 : [] --> A -> A -> A u182 : [] --> A -> A -> A u191 : [] --> A -> A -> A u201 : [] --> A -> A -> A -> A -> A u202 : [] --> A -> A -> A -> A -> A u203 : [] --> A -> A -> A -> A -> A u204 : [] --> A -> A -> A u21 : [] --> A -> A -> A -> A u211 : [] --> A -> A -> A u212 : [] --> A -> A -> A u22 : [] --> A -> A -> A u221 : [] --> A -> A -> A -> A u222 : [] --> A -> A -> A -> A u31 : [] --> A -> A -> A -> A u32 : [] --> A -> A -> A u41 : [] --> A -> A -> A u42 : [] --> A -> A u51 : [] --> A -> A -> A u52 : [] --> A -> A u61 : [] --> A -> A u71 : [] --> A -> A u81 : [] --> A -> A u91 : [] --> A -> A Rules: axxu101 tt x => axxu102 (axxisLNat x) axxu102 tt => tt axxu11 tt x y => axxu12 (axxisLNat y) x y axxu111 tt => tt axxu12 tt x y => axxsnd (axxsplitAt (mark x) (mark y)) axxu121 tt => tt axxu131 tt x => axxu132 (axxisLNat x) axxu132 tt => tt axxu141 tt x => axxu142 (axxisLNat x) axxu142 tt => tt axxu151 tt x => axxu152 (axxisLNat x) axxu152 tt => tt axxu161 tt x => cons (mark x) (natsFrom (s x)) axxu171 tt x y => axxu172 (axxisLNat y) x y axxu172 tt x y => axxhead (axxafterNth (mark x) (mark y)) axxu181 tt x => axxu182 (axxisLNat x) x axxu182 tt x => mark x axxu191 tt x => pair nil (mark x) axxu201 tt x y z => axxu202 (axxisNatural y) x y z axxu202 tt x y z => axxu203 (axxisLNat z) x y z axxu203 tt x y z => axxu204 (axxsplitAt (mark x) (mark z)) y axxu204 (pair x y) z => pair (cons (mark z) x) (mark y) axxu21 tt x y => axxu22 (axxisLNat y) x axxu211 tt x => axxu212 (axxisLNat x) x axxu212 tt x => mark x axxu22 tt x => mark x axxu221 tt x y => axxu222 (axxisLNat y) x y axxu222 tt x y => axxfst (axxsplitAt (mark x) (mark y)) axxu31 tt x y => axxu32 (axxisLNat y) x axxu32 tt x => mark x axxu41 tt x => axxu42 (axxisLNat x) axxu42 tt => tt axxu51 tt x => axxu52 (axxisLNat x) axxu52 tt => tt axxu61 tt => tt axxu71 tt => tt axxu81 tt => tt axxu91 tt => tt axxafterNth x y => axxu11 (axxisNatural x) x y axxfst (pair x y) => axxu21 (axxisLNat x) x y axxhead (cons x y) => axxu31 (axxisNatural x) x y axxisLNat nil => tt axxisLNat (afterNth x y) => axxu41 (axxisNatural x) y axxisLNat (cons x y) => axxu51 (axxisNatural x) y axxisLNat (fst x) => axxu61 (axxisPLNat x) axxisLNat (natsFrom x) => axxu71 (axxisNatural x) axxisLNat (snd x) => axxu81 (axxisPLNat x) axxisLNat (tail x) => axxu91 (axxisLNat x) axxisLNat (take x y) => axxu101 (axxisNatural x) y axxisNatural 0 => tt axxisNatural (head x) => axxu111 (axxisLNat x) axxisNatural (s x) => axxu121 (axxisNatural x) axxisNatural (sel x y) => axxu131 (axxisNatural x) y axxisPLNat (pair x y) => axxu141 (axxisLNat x) y axxisPLNat (splitAt x y) => axxu151 (axxisNatural x) y axxnatsFrom x => axxu161 (axxisNatural x) x axxsel x y => axxu171 (axxisNatural x) x y axxsnd (pair x y) => axxu181 (axxisLNat x) y axxsplitAt 0 x => axxu191 (axxisLNat x) x axxsplitAt (s x) (cons y z) => axxu201 (axxisNatural x) x y z axxtail (cons x y) => axxu211 (axxisNatural x) y axxtake x y => axxu221 (axxisNatural x) x y mark (u101 x y) => axxu101 (mark x) y mark (u102 x) => axxu102 (mark x) mark (isLNat x) => axxisLNat x mark (u11 x y z) => axxu11 (mark x) y z mark (u12 x y z) => axxu12 (mark x) y z mark (u111 x) => axxu111 (mark x) mark (snd x) => axxsnd (mark x) mark (splitAt x y) => axxsplitAt (mark x) (mark y) mark (u121 x) => axxu121 (mark x) mark (u131 x y) => axxu131 (mark x) y mark (u132 x) => axxu132 (mark x) mark (u141 x y) => axxu141 (mark x) y mark (u142 x) => axxu142 (mark x) mark (u151 x y) => axxu151 (mark x) y mark (u152 x) => axxu152 (mark x) mark (u161 x y) => axxu161 (mark x) y mark (natsFrom x) => axxnatsFrom (mark x) mark (u171 x y z) => axxu171 (mark x) y z mark (u172 x y z) => axxu172 (mark x) y z mark (head x) => axxhead (mark x) mark (afterNth x y) => axxafterNth (mark x) (mark y) mark (u181 x y) => axxu181 (mark x) y mark (u182 x y) => axxu182 (mark x) y mark (u191 x y) => axxu191 (mark x) y mark (u201 x y z u) => axxu201 (mark x) y z u mark (u202 x y z u) => axxu202 (mark x) y z u mark (isNatural x) => axxisNatural x mark (u203 x y z u) => axxu203 (mark x) y z u mark (u204 x y) => axxu204 (mark x) y mark (u21 x y z) => axxu21 (mark x) y z mark (u22 x y) => axxu22 (mark x) y mark (u211 x y) => axxu211 (mark x) y mark (u212 x y) => axxu212 (mark x) y mark (u221 x y z) => axxu221 (mark x) y z mark (u222 x y z) => axxu222 (mark x) y z mark (fst x) => axxfst (mark x) mark (u31 x y z) => axxu31 (mark x) y z mark (u32 x y) => axxu32 (mark x) y mark (u41 x y) => axxu41 (mark x) y mark (u42 x) => axxu42 (mark x) mark (u51 x y) => axxu51 (mark x) y mark (u52 x) => axxu52 (mark x) mark (u61 x) => axxu61 (mark x) mark (u71 x) => axxu71 (mark x) mark (u81 x) => axxu81 (mark x) mark (u91 x) => axxu91 (mark 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 => u101 x y axxu102 x => u102 x axxisLNat x => isLNat x axxu11 x y z => u11 x y z axxu12 x y z => u12 x y z axxu111 x => u111 x axxsnd x => snd x axxsplitAt x y => splitAt x y axxu121 x => u121 x axxu131 x y => u131 x y axxu132 x => u132 x axxu141 x y => u141 x y axxu142 x => u142 x axxu151 x y => u151 x y axxu152 x => u152 x axxu161 x y => u161 x y axxnatsFrom x => natsFrom x axxu171 x y z => u171 x y z axxu172 x y z => u172 x y z axxhead x => head x axxafterNth x y => afterNth x y axxu181 x y => u181 x y axxu182 x y => u182 x y axxu191 x y => u191 x y axxu201 x y z u => u201 x y z u axxu202 x y z u => u202 x y z u axxisNatural x => isNatural x axxu203 x y z u => u203 x y z u axxu204 x y => u204 x y axxu21 x y z => u21 x y z axxu22 x y => u22 x y axxu211 x y => u211 x y axxu212 x y => u212 x y axxu221 x y z => u221 x y z axxu222 x y z => u222 x y z axxfst x => fst x axxu31 x y z => u31 x y z axxu32 x y => u32 x y axxu41 x y => u41 x y axxu42 x => u42 x axxu51 x y => u51 x y axxu52 x => u52 x axxu61 x => u61 x axxu71 x => u71 x axxu81 x => u81 x axxu91 x => u91 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 app : [A -> A * A] --> A axxafterNth : [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 axxu102 : [A] --> A axxu11 : [A * A * A] --> A axxu111 : [A] --> A axxu12 : [A * A * A] --> A axxu121 : [A] --> A axxu131 : [A * A] --> A axxu132 : [A] --> A axxu141 : [A * A] --> A axxu142 : [A] --> A axxu151 : [A * A] --> A axxu152 : [A] --> A axxu161 : [A * A] --> A axxu171 : [A * A * A] --> A axxu172 : [A * A * A] --> A axxu181 : [A * A] --> A axxu182 : [A * A] --> A axxu191 : [A * A] --> A axxu201 : [A * A * A * A] --> A axxu202 : [A * A * A * A] --> A axxu203 : [A * A * A * A] --> A axxu204 : [A * A] --> A axxu21 : [A * A * A] --> A axxu211 : [A * A] --> A axxu212 : [A * A] --> A axxu22 : [A * A] --> A axxu221 : [A * A * A] --> A axxu222 : [A * A * A] --> A axxu31 : [A * A * A] --> A axxu32 : [A * A] --> A axxu41 : [A * A] --> A axxu42 : [A] --> A axxu51 : [A * A] --> A axxu52 : [A] --> A axxu61 : [A] --> A axxu71 : [A] --> A axxu81 : [A] --> A axxu91 : [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 u102 : [A] --> A u11 : [A * A * A] --> A u111 : [A] --> A u12 : [A * A * A] --> A u121 : [A] --> A u131 : [A * A] --> A u132 : [A] --> A u141 : [A * A] --> A u142 : [A] --> A u151 : [A * A] --> A u152 : [A] --> A u161 : [A * A] --> A u171 : [A * A * A] --> A u172 : [A * A * A] --> A u181 : [A * A] --> A u182 : [A * A] --> A u191 : [A * A] --> A u201 : [A * A * A * A] --> A u202 : [A * A * A * A] --> A u203 : [A * A * A * A] --> A u204 : [A * A] --> A u21 : [A * A * A] --> A u211 : [A * A] --> A u212 : [A * A] --> A u22 : [A * A] --> A u221 : [A * A * A] --> A u222 : [A * A * A] --> A u31 : [A * A * A] --> A u32 : [A * A] --> A u41 : [A * A] --> A u42 : [A] --> A u51 : [A * A] --> A u52 : [A] --> A u61 : [A] --> A u71 : [A] --> A u81 : [A] --> A u91 : [A] --> A ~AP1 : [A -> A * A] --> A Rules: axxu101(tt, X) => axxu102(axxisLNat(X)) axxu102(tt) => tt axxu11(tt, X, Y) => axxu12(axxisLNat(Y), X, Y) axxu111(tt) => tt axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) axxu121(tt) => tt axxu131(tt, X) => axxu132(axxisLNat(X)) axxu132(tt) => tt axxu141(tt, X) => axxu142(axxisLNat(X)) axxu142(tt) => tt axxu151(tt, X) => axxu152(axxisLNat(X)) axxu152(tt) => tt axxu161(tt, X) => cons(mark(X), natsFrom(s(X))) axxu171(tt, X, Y) => axxu172(axxisLNat(Y), X, Y) axxu172(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) axxu181(tt, X) => axxu182(axxisLNat(X), X) axxu182(tt, X) => mark(X) axxu191(tt, X) => pair(nil, mark(X)) axxu201(tt, X, Y, Z) => axxu202(axxisNatural(Y), X, Y, Z) axxu202(tt, X, Y, Z) => axxu203(axxisLNat(Z), X, Y, Z) axxu203(tt, X, Y, Z) => axxu204(axxsplitAt(mark(X), mark(Z)), Y) axxu204(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) axxu21(tt, X, Y) => axxu22(axxisLNat(Y), X) axxu211(tt, X) => axxu212(axxisLNat(X), X) axxu212(tt, X) => mark(X) axxu22(tt, X) => mark(X) axxu221(tt, X, Y) => axxu222(axxisLNat(Y), X, Y) axxu222(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) axxu31(tt, X, Y) => axxu32(axxisLNat(Y), X) axxu32(tt, X) => mark(X) axxu41(tt, X) => axxu42(axxisLNat(X)) axxu42(tt) => tt axxu51(tt, X) => axxu52(axxisLNat(X)) axxu52(tt) => tt axxu61(tt) => tt axxu71(tt) => tt axxu81(tt) => tt axxu91(tt) => tt axxafterNth(X, Y) => axxu11(axxisNatural(X), X, Y) axxfst(pair(X, Y)) => axxu21(axxisLNat(X), X, Y) axxhead(cons(X, Y)) => axxu31(axxisNatural(X), X, Y) axxisLNat(nil) => tt axxisLNat(afterNth(X, Y)) => axxu41(axxisNatural(X), Y) axxisLNat(cons(X, Y)) => axxu51(axxisNatural(X), Y) axxisLNat(fst(X)) => axxu61(axxisPLNat(X)) axxisLNat(natsFrom(X)) => axxu71(axxisNatural(X)) axxisLNat(snd(X)) => axxu81(axxisPLNat(X)) axxisLNat(tail(X)) => axxu91(axxisLNat(X)) axxisLNat(take(X, Y)) => axxu101(axxisNatural(X), Y) axxisNatural(0) => tt axxisNatural(head(X)) => axxu111(axxisLNat(X)) axxisNatural(s(X)) => axxu121(axxisNatural(X)) axxisNatural(sel(X, Y)) => axxu131(axxisNatural(X), Y) axxisPLNat(pair(X, Y)) => axxu141(axxisLNat(X), Y) axxisPLNat(splitAt(X, Y)) => axxu151(axxisNatural(X), Y) axxnatsFrom(X) => axxu161(axxisNatural(X), X) axxsel(X, Y) => axxu171(axxisNatural(X), X, Y) axxsnd(pair(X, Y)) => axxu181(axxisLNat(X), Y) axxsplitAt(0, X) => axxu191(axxisLNat(X), X) axxsplitAt(s(X), cons(Y, Z)) => axxu201(axxisNatural(X), X, Y, Z) axxtail(cons(X, Y)) => axxu211(axxisNatural(X), Y) axxtake(X, Y) => axxu221(axxisNatural(X), X, Y) mark(u101(X, Y)) => axxu101(mark(X), Y) mark(u102(X)) => axxu102(mark(X)) mark(isLNat(X)) => axxisLNat(X) mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) mark(u111(X)) => axxu111(mark(X)) mark(snd(X)) => axxsnd(mark(X)) mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) mark(u121(X)) => axxu121(mark(X)) mark(u131(X, Y)) => axxu131(mark(X), Y) mark(u132(X)) => axxu132(mark(X)) mark(u141(X, Y)) => axxu141(mark(X), Y) mark(u142(X)) => axxu142(mark(X)) mark(u151(X, Y)) => axxu151(mark(X), Y) mark(u152(X)) => axxu152(mark(X)) mark(u161(X, Y)) => axxu161(mark(X), Y) mark(natsFrom(X)) => axxnatsFrom(mark(X)) mark(u171(X, Y, Z)) => axxu171(mark(X), Y, Z) mark(u172(X, Y, Z)) => axxu172(mark(X), Y, Z) mark(head(X)) => axxhead(mark(X)) mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) mark(u181(X, Y)) => axxu181(mark(X), Y) mark(u182(X, Y)) => axxu182(mark(X), Y) mark(u191(X, Y)) => axxu191(mark(X), Y) mark(u201(X, Y, Z, U)) => axxu201(mark(X), Y, Z, U) mark(u202(X, Y, Z, U)) => axxu202(mark(X), Y, Z, U) mark(isNatural(X)) => axxisNatural(X) mark(u203(X, Y, Z, U)) => axxu203(mark(X), Y, Z, U) mark(u204(X, Y)) => axxu204(mark(X), Y) mark(u21(X, Y, Z)) => axxu21(mark(X), Y, Z) mark(u22(X, Y)) => axxu22(mark(X), Y) mark(u211(X, Y)) => axxu211(mark(X), Y) mark(u212(X, Y)) => axxu212(mark(X), Y) mark(u221(X, Y, Z)) => axxu221(mark(X), Y, Z) mark(u222(X, Y, Z)) => axxu222(mark(X), Y, Z) mark(fst(X)) => axxfst(mark(X)) mark(u31(X, Y, Z)) => axxu31(mark(X), Y, Z) mark(u32(X, Y)) => axxu32(mark(X), Y) mark(u41(X, Y)) => axxu41(mark(X), Y) mark(u42(X)) => axxu42(mark(X)) mark(u51(X, Y)) => axxu51(mark(X), Y) mark(u52(X)) => axxu52(mark(X)) mark(u61(X)) => axxu61(mark(X)) mark(u71(X)) => axxu71(mark(X)) mark(u81(X)) => axxu81(mark(X)) mark(u91(X)) => axxu91(mark(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) => u101(X, Y) axxu102(X) => u102(X) axxisLNat(X) => isLNat(X) axxu11(X, Y, Z) => u11(X, Y, Z) axxu12(X, Y, Z) => u12(X, Y, Z) axxu111(X) => u111(X) axxsnd(X) => snd(X) axxsplitAt(X, Y) => splitAt(X, Y) axxu121(X) => u121(X) axxu131(X, Y) => u131(X, Y) axxu132(X) => u132(X) axxu141(X, Y) => u141(X, Y) axxu142(X) => u142(X) axxu151(X, Y) => u151(X, Y) axxu152(X) => u152(X) axxu161(X, Y) => u161(X, Y) axxnatsFrom(X) => natsFrom(X) axxu171(X, Y, Z) => u171(X, Y, Z) axxu172(X, Y, Z) => u172(X, Y, Z) axxhead(X) => head(X) axxafterNth(X, Y) => afterNth(X, Y) axxu181(X, Y) => u181(X, Y) axxu182(X, Y) => u182(X, Y) axxu191(X, Y) => u191(X, Y) axxu201(X, Y, Z, U) => u201(X, Y, Z, U) axxu202(X, Y, Z, U) => u202(X, Y, Z, U) axxisNatural(X) => isNatural(X) axxu203(X, Y, Z, U) => u203(X, Y, Z, U) axxu204(X, Y) => u204(X, Y) axxu21(X, Y, Z) => u21(X, Y, Z) axxu22(X, Y) => u22(X, Y) axxu211(X, Y) => u211(X, Y) axxu212(X, Y) => u212(X, Y) axxu221(X, Y, Z) => u221(X, Y, Z) axxu222(X, Y, Z) => u222(X, Y, Z) axxfst(X) => fst(X) axxu31(X, Y, Z) => u31(X, Y, Z) axxu32(X, Y) => u32(X, Y) axxu41(X, Y) => u41(X, Y) axxu42(X) => u42(X) axxu51(X, Y) => u51(X, Y) axxu52(X) => u52(X) axxu61(X) => u61(X) axxu71(X) => u71(X) axxu81(X) => u81(X) axxu91(X) => u91(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.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.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, x), nil) => nil map(/\x.axxu102(x), nil) => nil map(/\x.axxu11(X, Y, x), nil) => nil map(/\x.axxu111(x), nil) => nil map(/\x.axxu12(X, Y, x), nil) => nil map(/\x.axxu121(x), nil) => nil map(/\x.axxu131(X, x), nil) => nil map(/\x.axxu132(x), nil) => nil map(/\x.axxu141(X, x), nil) => nil map(/\x.axxu142(x), nil) => nil map(/\x.axxu151(X, x), nil) => nil map(/\x.axxu152(x), nil) => nil map(/\x.axxu161(X, x), nil) => nil map(/\x.axxu171(X, Y, x), nil) => nil map(/\x.axxu172(X, Y, x), nil) => nil map(/\x.axxu181(X, x), nil) => nil map(/\x.axxu182(X, x), nil) => nil map(/\x.axxu191(X, x), nil) => nil map(/\x.axxu201(X, Y, Z, x), nil) => nil map(/\x.axxu202(X, Y, Z, x), nil) => nil map(/\x.axxu203(X, Y, Z, x), nil) => nil map(/\x.axxu204(X, x), nil) => nil map(/\x.axxu21(X, Y, x), nil) => nil map(/\x.axxu211(X, x), nil) => nil map(/\x.axxu212(X, x), nil) => nil map(/\x.axxu22(X, x), nil) => nil map(/\x.axxu221(X, Y, x), nil) => nil map(/\x.axxu222(X, Y, x), nil) => nil map(/\x.axxu31(X, Y, x), nil) => nil map(/\x.axxu32(X, x), nil) => nil map(/\x.axxu41(X, x), nil) => nil map(/\x.axxu42(x), nil) => nil map(/\x.axxu51(X, x), nil) => nil map(/\x.axxu52(x), nil) => nil map(/\x.axxu61(x), nil) => nil map(/\x.axxu71(x), nil) => nil map(/\x.axxu81(x), nil) => nil map(/\x.axxu91(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, x), nil) => nil map(/\x.u102(x), nil) => nil map(/\x.u11(X, Y, x), nil) => nil map(/\x.u111(x), nil) => nil map(/\x.u12(X, Y, x), nil) => nil map(/\x.u121(x), nil) => nil map(/\x.u131(X, x), nil) => nil map(/\x.u132(x), nil) => nil map(/\x.u141(X, x), nil) => nil map(/\x.u142(x), nil) => nil map(/\x.u151(X, x), nil) => nil map(/\x.u152(x), nil) => nil map(/\x.u161(X, x), nil) => nil map(/\x.u171(X, Y, x), nil) => nil map(/\x.u172(X, Y, x), nil) => nil map(/\x.u181(X, x), nil) => nil map(/\x.u182(X, x), nil) => nil map(/\x.u191(X, x), nil) => nil map(/\x.u201(X, Y, Z, x), nil) => nil map(/\x.u202(X, Y, Z, x), nil) => nil map(/\x.u203(X, Y, Z, x), nil) => nil map(/\x.u204(X, x), nil) => nil map(/\x.u21(X, Y, x), nil) => nil map(/\x.u211(X, x), nil) => nil map(/\x.u212(X, x), nil) => nil map(/\x.u22(X, x), nil) => nil map(/\x.u221(X, Y, x), nil) => nil map(/\x.u222(X, Y, x), nil) => nil map(/\x.u31(X, Y, x), nil) => nil map(/\x.u32(X, x), nil) => nil map(/\x.u41(X, x), nil) => nil map(/\x.u42(x), nil) => nil map(/\x.u51(X, x), nil) => nil map(/\x.u52(x), nil) => nil map(/\x.u61(x), nil) => nil map(/\x.u71(x), nil) => nil map(/\x.u81(x), nil) => nil map(/\x.u91(x), nil) => nil 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.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, x), Y) => axxu101(X, Y) app(/\x.axxu102(x), X) => axxu102(X) app(/\x.axxu11(X, Y, x), Z) => axxu11(X, Y, Z) app(/\x.axxu111(x), X) => axxu111(X) app(/\x.axxu12(X, Y, x), Z) => axxu12(X, Y, Z) app(/\x.axxu121(x), X) => axxu121(X) app(/\x.axxu131(X, x), Y) => axxu131(X, Y) app(/\x.axxu132(x), X) => axxu132(X) app(/\x.axxu141(X, x), Y) => axxu141(X, Y) app(/\x.axxu142(x), X) => axxu142(X) app(/\x.axxu151(X, x), Y) => axxu151(X, Y) app(/\x.axxu152(x), X) => axxu152(X) app(/\x.axxu161(X, x), Y) => axxu161(X, Y) app(/\x.axxu171(X, Y, x), Z) => axxu171(X, Y, Z) app(/\x.axxu172(X, Y, x), Z) => axxu172(X, Y, Z) app(/\x.axxu181(X, x), Y) => axxu181(X, Y) app(/\x.axxu182(X, x), Y) => axxu182(X, Y) app(/\x.axxu191(X, x), Y) => axxu191(X, Y) app(/\x.axxu201(X, Y, Z, x), U) => axxu201(X, Y, Z, U) app(/\x.axxu202(X, Y, Z, x), U) => axxu202(X, Y, Z, U) app(/\x.axxu203(X, Y, Z, x), U) => axxu203(X, Y, Z, U) app(/\x.axxu204(X, x), Y) => axxu204(X, Y) app(/\x.axxu21(X, Y, x), Z) => axxu21(X, Y, Z) app(/\x.axxu211(X, x), Y) => axxu211(X, Y) app(/\x.axxu212(X, x), Y) => axxu212(X, Y) app(/\x.axxu22(X, x), Y) => axxu22(X, Y) app(/\x.axxu221(X, Y, x), Z) => axxu221(X, Y, Z) app(/\x.axxu222(X, Y, x), Z) => axxu222(X, Y, Z) app(/\x.axxu31(X, Y, x), Z) => axxu31(X, Y, Z) app(/\x.axxu32(X, x), Y) => axxu32(X, Y) app(/\x.axxu41(X, x), Y) => axxu41(X, Y) app(/\x.axxu42(x), X) => axxu42(X) app(/\x.axxu51(X, x), Y) => axxu51(X, Y) app(/\x.axxu52(x), X) => axxu52(X) app(/\x.axxu61(x), X) => axxu61(X) app(/\x.axxu71(x), X) => axxu71(X) app(/\x.axxu81(x), X) => axxu81(X) app(/\x.axxu91(x), X) => axxu91(X) 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, x), Y) => u101(X, Y) app(/\x.u102(x), X) => u102(X) app(/\x.u11(X, Y, x), Z) => u11(X, Y, Z) app(/\x.u111(x), X) => u111(X) app(/\x.u12(X, Y, x), Z) => u12(X, Y, Z) app(/\x.u121(x), X) => u121(X) app(/\x.u131(X, x), Y) => u131(X, Y) app(/\x.u132(x), X) => u132(X) app(/\x.u141(X, x), Y) => u141(X, Y) app(/\x.u142(x), X) => u142(X) app(/\x.u151(X, x), Y) => u151(X, Y) app(/\x.u152(x), X) => u152(X) app(/\x.u161(X, x), Y) => u161(X, Y) app(/\x.u171(X, Y, x), Z) => u171(X, Y, Z) app(/\x.u172(X, Y, x), Z) => u172(X, Y, Z) app(/\x.u181(X, x), Y) => u181(X, Y) app(/\x.u182(X, x), Y) => u182(X, Y) app(/\x.u191(X, x), Y) => u191(X, Y) app(/\x.u201(X, Y, Z, x), U) => u201(X, Y, Z, U) app(/\x.u202(X, Y, Z, x), U) => u202(X, Y, Z, U) app(/\x.u203(X, Y, Z, x), U) => u203(X, Y, Z, U) app(/\x.u204(X, x), Y) => u204(X, Y) app(/\x.u21(X, Y, x), Z) => u21(X, Y, Z) app(/\x.u211(X, x), Y) => u211(X, Y) app(/\x.u212(X, x), Y) => u212(X, Y) app(/\x.u22(X, x), Y) => u22(X, Y) app(/\x.u221(X, Y, x), Z) => u221(X, Y, Z) app(/\x.u222(X, Y, x), Z) => u222(X, Y, Z) app(/\x.u31(X, Y, x), Z) => u31(X, Y, Z) app(/\x.u32(X, x), Y) => u32(X, Y) app(/\x.u41(X, x), Y) => u41(X, Y) app(/\x.u42(x), X) => u42(X) app(/\x.u51(X, x), Y) => u51(X, Y) app(/\x.u52(x), X) => u52(X) app(/\x.u61(x), X) => u61(X) app(/\x.u71(x), X) => u71(X) app(/\x.u81(x), X) => u81(X) app(/\x.u91(x), X) => u91(X) ~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 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 axxu102 : [A] --> A axxu11 : [A * A * A] --> A axxu111 : [A] --> A axxu12 : [A * A * A] --> A axxu121 : [A] --> A axxu131 : [A * A] --> A axxu132 : [A] --> A axxu141 : [A * A] --> A axxu142 : [A] --> A axxu151 : [A * A] --> A axxu152 : [A] --> A axxu161 : [A * A] --> A axxu171 : [A * A * A] --> A axxu172 : [A * A * A] --> A axxu181 : [A * A] --> A axxu182 : [A * A] --> A axxu191 : [A * A] --> A axxu201 : [A * A * A * A] --> A axxu202 : [A * A * A * A] --> A axxu203 : [A * A * A * A] --> A axxu204 : [A * A] --> A axxu21 : [A * A * A] --> A axxu211 : [A * A] --> A axxu212 : [A * A] --> A axxu22 : [A * A] --> A axxu221 : [A * A * A] --> A axxu222 : [A * A * A] --> A axxu31 : [A * A * A] --> A axxu32 : [A * A] --> A axxu41 : [A * A] --> A axxu42 : [A] --> A axxu51 : [A * A] --> A axxu52 : [A] --> A axxu61 : [A] --> A axxu71 : [A] --> A axxu81 : [A] --> A axxu91 : [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 u102 : [A] --> A u11 : [A * A * A] --> A u111 : [A] --> A u12 : [A * A * A] --> A u121 : [A] --> A u131 : [A * A] --> A u132 : [A] --> A u141 : [A * A] --> A u142 : [A] --> A u151 : [A * A] --> A u152 : [A] --> A u161 : [A * A] --> A u171 : [A * A * A] --> A u172 : [A * A * A] --> A u181 : [A * A] --> A u182 : [A * A] --> A u191 : [A * A] --> A u201 : [A * A * A * A] --> A u202 : [A * A * A * A] --> A u203 : [A * A * A * A] --> A u204 : [A * A] --> A u21 : [A * A * A] --> A u211 : [A * A] --> A u212 : [A * A] --> A u22 : [A * A] --> A u221 : [A * A * A] --> A u222 : [A * A * A] --> A u31 : [A * A * A] --> A u32 : [A * A] --> A u41 : [A * A] --> A u42 : [A] --> A u51 : [A * A] --> A u52 : [A] --> A u61 : [A] --> A u71 : [A] --> A u81 : [A] --> A u91 : [A] --> A Rules: axxu101(tt, X) => axxu102(axxisLNat(X)) axxu102(tt) => tt axxu11(tt, X, Y) => axxu12(axxisLNat(Y), X, Y) axxu111(tt) => tt axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) axxu121(tt) => tt axxu131(tt, X) => axxu132(axxisLNat(X)) axxu132(tt) => tt axxu141(tt, X) => axxu142(axxisLNat(X)) axxu142(tt) => tt axxu151(tt, X) => axxu152(axxisLNat(X)) axxu152(tt) => tt axxu161(tt, X) => cons(mark(X), natsFrom(s(X))) axxu171(tt, X, Y) => axxu172(axxisLNat(Y), X, Y) axxu172(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) axxu181(tt, X) => axxu182(axxisLNat(X), X) axxu182(tt, X) => mark(X) axxu191(tt, X) => pair(nil, mark(X)) axxu201(tt, X, Y, Z) => axxu202(axxisNatural(Y), X, Y, Z) axxu202(tt, X, Y, Z) => axxu203(axxisLNat(Z), X, Y, Z) axxu203(tt, X, Y, Z) => axxu204(axxsplitAt(mark(X), mark(Z)), Y) axxu204(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) axxu21(tt, X, Y) => axxu22(axxisLNat(Y), X) axxu211(tt, X) => axxu212(axxisLNat(X), X) axxu212(tt, X) => mark(X) axxu22(tt, X) => mark(X) axxu221(tt, X, Y) => axxu222(axxisLNat(Y), X, Y) axxu222(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) axxu31(tt, X, Y) => axxu32(axxisLNat(Y), X) axxu32(tt, X) => mark(X) axxu41(tt, X) => axxu42(axxisLNat(X)) axxu42(tt) => tt axxu51(tt, X) => axxu52(axxisLNat(X)) axxu52(tt) => tt axxu61(tt) => tt axxu71(tt) => tt axxu81(tt) => tt axxu91(tt) => tt axxafterNth(X, Y) => axxu11(axxisNatural(X), X, Y) axxfst(pair(X, Y)) => axxu21(axxisLNat(X), X, Y) axxhead(cons(X, Y)) => axxu31(axxisNatural(X), X, Y) axxisLNat(nil) => tt axxisLNat(afterNth(X, Y)) => axxu41(axxisNatural(X), Y) axxisLNat(cons(X, Y)) => axxu51(axxisNatural(X), Y) axxisLNat(fst(X)) => axxu61(axxisPLNat(X)) axxisLNat(natsFrom(X)) => axxu71(axxisNatural(X)) axxisLNat(snd(X)) => axxu81(axxisPLNat(X)) axxisLNat(tail(X)) => axxu91(axxisLNat(X)) axxisLNat(take(X, Y)) => axxu101(axxisNatural(X), Y) axxisNatural(0) => tt axxisNatural(head(X)) => axxu111(axxisLNat(X)) axxisNatural(s(X)) => axxu121(axxisNatural(X)) axxisNatural(sel(X, Y)) => axxu131(axxisNatural(X), Y) axxisPLNat(pair(X, Y)) => axxu141(axxisLNat(X), Y) axxisPLNat(splitAt(X, Y)) => axxu151(axxisNatural(X), Y) axxnatsFrom(X) => axxu161(axxisNatural(X), X) axxsel(X, Y) => axxu171(axxisNatural(X), X, Y) axxsnd(pair(X, Y)) => axxu181(axxisLNat(X), Y) axxsplitAt(0, X) => axxu191(axxisLNat(X), X) axxsplitAt(s(X), cons(Y, Z)) => axxu201(axxisNatural(X), X, Y, Z) axxtail(cons(X, Y)) => axxu211(axxisNatural(X), Y) axxtake(X, Y) => axxu221(axxisNatural(X), X, Y) mark(u101(X, Y)) => axxu101(mark(X), Y) mark(u102(X)) => axxu102(mark(X)) mark(isLNat(X)) => axxisLNat(X) mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) mark(u111(X)) => axxu111(mark(X)) mark(snd(X)) => axxsnd(mark(X)) mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) mark(u121(X)) => axxu121(mark(X)) mark(u131(X, Y)) => axxu131(mark(X), Y) mark(u132(X)) => axxu132(mark(X)) mark(u141(X, Y)) => axxu141(mark(X), Y) mark(u142(X)) => axxu142(mark(X)) mark(u151(X, Y)) => axxu151(mark(X), Y) mark(u152(X)) => axxu152(mark(X)) mark(u161(X, Y)) => axxu161(mark(X), Y) mark(natsFrom(X)) => axxnatsFrom(mark(X)) mark(u171(X, Y, Z)) => axxu171(mark(X), Y, Z) mark(u172(X, Y, Z)) => axxu172(mark(X), Y, Z) mark(head(X)) => axxhead(mark(X)) mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) mark(u181(X, Y)) => axxu181(mark(X), Y) mark(u182(X, Y)) => axxu182(mark(X), Y) mark(u191(X, Y)) => axxu191(mark(X), Y) mark(u201(X, Y, Z, U)) => axxu201(mark(X), Y, Z, U) mark(u202(X, Y, Z, U)) => axxu202(mark(X), Y, Z, U) mark(isNatural(X)) => axxisNatural(X) mark(u203(X, Y, Z, U)) => axxu203(mark(X), Y, Z, U) mark(u204(X, Y)) => axxu204(mark(X), Y) mark(u21(X, Y, Z)) => axxu21(mark(X), Y, Z) mark(u22(X, Y)) => axxu22(mark(X), Y) mark(u211(X, Y)) => axxu211(mark(X), Y) mark(u212(X, Y)) => axxu212(mark(X), Y) mark(u221(X, Y, Z)) => axxu221(mark(X), Y, Z) mark(u222(X, Y, Z)) => axxu222(mark(X), Y, Z) mark(fst(X)) => axxfst(mark(X)) mark(u31(X, Y, Z)) => axxu31(mark(X), Y, Z) mark(u32(X, Y)) => axxu32(mark(X), Y) mark(u41(X, Y)) => axxu41(mark(X), Y) mark(u42(X)) => axxu42(mark(X)) mark(u51(X, Y)) => axxu51(mark(X), Y) mark(u52(X)) => axxu52(mark(X)) mark(u61(X)) => axxu61(mark(X)) mark(u71(X)) => axxu71(mark(X)) mark(u81(X)) => axxu81(mark(X)) mark(u91(X)) => axxu91(mark(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) => u101(X, Y) axxu102(X) => u102(X) axxisLNat(X) => isLNat(X) axxu11(X, Y, Z) => u11(X, Y, Z) axxu12(X, Y, Z) => u12(X, Y, Z) axxu111(X) => u111(X) axxsnd(X) => snd(X) axxsplitAt(X, Y) => splitAt(X, Y) axxu121(X) => u121(X) axxu131(X, Y) => u131(X, Y) axxu132(X) => u132(X) axxu141(X, Y) => u141(X, Y) axxu142(X) => u142(X) axxu151(X, Y) => u151(X, Y) axxu152(X) => u152(X) axxu161(X, Y) => u161(X, Y) axxnatsFrom(X) => natsFrom(X) axxu171(X, Y, Z) => u171(X, Y, Z) axxu172(X, Y, Z) => u172(X, Y, Z) axxhead(X) => head(X) axxafterNth(X, Y) => afterNth(X, Y) axxu181(X, Y) => u181(X, Y) axxu182(X, Y) => u182(X, Y) axxu191(X, Y) => u191(X, Y) axxu201(X, Y, Z, U) => u201(X, Y, Z, U) axxu202(X, Y, Z, U) => u202(X, Y, Z, U) axxisNatural(X) => isNatural(X) axxu203(X, Y, Z, U) => u203(X, Y, Z, U) axxu204(X, Y) => u204(X, Y) axxu21(X, Y, Z) => u21(X, Y, Z) axxu22(X, Y) => u22(X, Y) axxu211(X, Y) => u211(X, Y) axxu212(X, Y) => u212(X, Y) axxu221(X, Y, Z) => u221(X, Y, Z) axxu222(X, Y, Z) => u222(X, Y, Z) axxfst(X) => fst(X) axxu31(X, Y, Z) => u31(X, Y, Z) axxu32(X, Y) => u32(X, Y) axxu41(X, Y) => u41(X, Y) axxu42(X) => u42(X) axxu51(X, Y) => u51(X, Y) axxu52(X) => u52(X) axxu61(X) => u61(X) axxu71(X) => u71(X) axxu81(X) => u81(X) axxu91(X) => u91(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) => axxu102(axxisLNat(X)) axxu102(tt) => tt axxu11(tt, X, Y) => axxu12(axxisLNat(Y), X, Y) axxu111(tt) => tt axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) axxu121(tt) => tt axxu131(tt, X) => axxu132(axxisLNat(X)) axxu132(tt) => tt axxu141(tt, X) => axxu142(axxisLNat(X)) axxu142(tt) => tt axxu151(tt, X) => axxu152(axxisLNat(X)) axxu152(tt) => tt axxu161(tt, X) => cons(mark(X), natsFrom(s(X))) axxu171(tt, X, Y) => axxu172(axxisLNat(Y), X, Y) axxu172(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) axxu181(tt, X) => axxu182(axxisLNat(X), X) axxu182(tt, X) => mark(X) axxu191(tt, X) => pair(nil, mark(X)) axxu201(tt, X, Y, Z) => axxu202(axxisNatural(Y), X, Y, Z) axxu202(tt, X, Y, Z) => axxu203(axxisLNat(Z), X, Y, Z) axxu203(tt, X, Y, Z) => axxu204(axxsplitAt(mark(X), mark(Z)), Y) axxu204(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) axxu21(tt, X, Y) => axxu22(axxisLNat(Y), X) axxu211(tt, X) => axxu212(axxisLNat(X), X) axxu212(tt, X) => mark(X) axxu22(tt, X) => mark(X) axxu221(tt, X, Y) => axxu222(axxisLNat(Y), X, Y) axxu222(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) axxu31(tt, X, Y) => axxu32(axxisLNat(Y), X) axxu32(tt, X) => mark(X) axxu41(tt, X) => axxu42(axxisLNat(X)) axxu42(tt) => tt axxu51(tt, X) => axxu52(axxisLNat(X)) axxu52(tt) => tt axxu61(tt) => tt axxu71(tt) => tt axxu81(tt) => tt axxu91(tt) => tt axxafterNth(X, Y) => axxu11(axxisNatural(X), X, Y) axxfst(pair(X, Y)) => axxu21(axxisLNat(X), X, Y) axxhead(cons(X, Y)) => axxu31(axxisNatural(X), X, Y) axxisLNat(nil) => tt axxisLNat(afterNth(X, Y)) => axxu41(axxisNatural(X), Y) axxisLNat(cons(X, Y)) => axxu51(axxisNatural(X), Y) axxisLNat(fst(X)) => axxu61(axxisPLNat(X)) axxisLNat(natsFrom(X)) => axxu71(axxisNatural(X)) axxisLNat(snd(X)) => axxu81(axxisPLNat(X)) axxisLNat(tail(X)) => axxu91(axxisLNat(X)) axxisLNat(take(X, Y)) => axxu101(axxisNatural(X), Y) axxisNatural(0) => tt axxisNatural(head(X)) => axxu111(axxisLNat(X)) axxisNatural(s(X)) => axxu121(axxisNatural(X)) axxisNatural(sel(X, Y)) => axxu131(axxisNatural(X), Y) axxisPLNat(pair(X, Y)) => axxu141(axxisLNat(X), Y) axxisPLNat(splitAt(X, Y)) => axxu151(axxisNatural(X), Y) axxnatsFrom(X) => axxu161(axxisNatural(X), X) axxsel(X, Y) => axxu171(axxisNatural(X), X, Y) axxsnd(pair(X, Y)) => axxu181(axxisLNat(X), Y) axxsplitAt(0, X) => axxu191(axxisLNat(X), X) axxsplitAt(s(X), cons(Y, Z)) => axxu201(axxisNatural(X), X, Y, Z) axxtail(cons(X, Y)) => axxu211(axxisNatural(X), Y) axxtake(X, Y) => axxu221(axxisNatural(X), X, Y) mark(u101(X, Y)) => axxu101(mark(X), Y) mark(u102(X)) => axxu102(mark(X)) mark(isLNat(X)) => axxisLNat(X) mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) mark(u111(X)) => axxu111(mark(X)) mark(snd(X)) => axxsnd(mark(X)) mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) mark(u121(X)) => axxu121(mark(X)) mark(u131(X, Y)) => axxu131(mark(X), Y) mark(u132(X)) => axxu132(mark(X)) mark(u141(X, Y)) => axxu141(mark(X), Y) mark(u142(X)) => axxu142(mark(X)) mark(u151(X, Y)) => axxu151(mark(X), Y) mark(u152(X)) => axxu152(mark(X)) mark(u161(X, Y)) => axxu161(mark(X), Y) mark(natsFrom(X)) => axxnatsFrom(mark(X)) mark(u171(X, Y, Z)) => axxu171(mark(X), Y, Z) mark(u172(X, Y, Z)) => axxu172(mark(X), Y, Z) mark(head(X)) => axxhead(mark(X)) mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) mark(u181(X, Y)) => axxu181(mark(X), Y) mark(u182(X, Y)) => axxu182(mark(X), Y) mark(u191(X, Y)) => axxu191(mark(X), Y) mark(u201(X, Y, Z, U)) => axxu201(mark(X), Y, Z, U) mark(u202(X, Y, Z, U)) => axxu202(mark(X), Y, Z, U) mark(isNatural(X)) => axxisNatural(X) mark(u203(X, Y, Z, U)) => axxu203(mark(X), Y, Z, U) mark(u204(X, Y)) => axxu204(mark(X), Y) mark(u21(X, Y, Z)) => axxu21(mark(X), Y, Z) mark(u22(X, Y)) => axxu22(mark(X), Y) mark(u211(X, Y)) => axxu211(mark(X), Y) mark(u212(X, Y)) => axxu212(mark(X), Y) mark(u221(X, Y, Z)) => axxu221(mark(X), Y, Z) mark(u222(X, Y, Z)) => axxu222(mark(X), Y, Z) mark(fst(X)) => axxfst(mark(X)) mark(u31(X, Y, Z)) => axxu31(mark(X), Y, Z) mark(u32(X, Y)) => axxu32(mark(X), Y) mark(u41(X, Y)) => axxu41(mark(X), Y) mark(u42(X)) => axxu42(mark(X)) mark(u51(X, Y)) => axxu51(mark(X), Y) mark(u52(X)) => axxu52(mark(X)) mark(u61(X)) => axxu61(mark(X)) mark(u71(X)) => axxu71(mark(X)) mark(u81(X)) => axxu81(mark(X)) mark(u91(X)) => axxu91(mark(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) => u101(X, Y) axxu102(X) => u102(X) axxisLNat(X) => isLNat(X) axxu11(X, Y, Z) => u11(X, Y, Z) axxu12(X, Y, Z) => u12(X, Y, Z) axxu111(X) => u111(X) axxsnd(X) => snd(X) axxsplitAt(X, Y) => splitAt(X, Y) axxu121(X) => u121(X) axxu131(X, Y) => u131(X, Y) axxu132(X) => u132(X) axxu141(X, Y) => u141(X, Y) axxu142(X) => u142(X) axxu151(X, Y) => u151(X, Y) axxu152(X) => u152(X) axxu161(X, Y) => u161(X, Y) axxnatsFrom(X) => natsFrom(X) axxu171(X, Y, Z) => u171(X, Y, Z) axxu172(X, Y, Z) => u172(X, Y, Z) axxhead(X) => head(X) axxafterNth(X, Y) => afterNth(X, Y) axxu181(X, Y) => u181(X, Y) axxu182(X, Y) => u182(X, Y) axxu191(X, Y) => u191(X, Y) axxu201(X, Y, Z, U) => u201(X, Y, Z, U) axxu202(X, Y, Z, U) => u202(X, Y, Z, U) axxisNatural(X) => isNatural(X) axxu203(X, Y, Z, U) => u203(X, Y, Z, U) axxu204(X, Y) => u204(X, Y) axxu21(X, Y, Z) => u21(X, Y, Z) axxu22(X, Y) => u22(X, Y) axxu211(X, Y) => u211(X, Y) axxu212(X, Y) => u212(X, Y) axxu221(X, Y, Z) => u221(X, Y, Z) axxu222(X, Y, Z) => u222(X, Y, Z) axxfst(X) => fst(X) axxu31(X, Y, Z) => u31(X, Y, Z) axxu32(X, Y) => u32(X, Y) axxu41(X, Y) => u41(X, Y) axxu42(X) => u42(X) axxu51(X, Y) => u51(X, Y) axxu52(X) => u52(X) axxu61(X) => u61(X) axxu71(X) => u71(X) axxu81(X) => u81(X) axxu91(X) => u91(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) -> axxu102(axxisLNat(PeRCenTX)) || 2: axxu102(tt()) -> tt() || 3: axxu11(tt(),PeRCenTX,PeRCenTY) -> axxu12(axxisLNat(PeRCenTY),PeRCenTX,PeRCenTY) || 4: axxu111(tt()) -> tt() || 5: axxu12(tt(),PeRCenTX,PeRCenTY) -> axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))) || 6: axxu121(tt()) -> tt() || 7: axxu131(tt(),PeRCenTX) -> axxu132(axxisLNat(PeRCenTX)) || 8: axxu132(tt()) -> tt() || 9: axxu141(tt(),PeRCenTX) -> axxu142(axxisLNat(PeRCenTX)) || 10: axxu142(tt()) -> tt() || 11: axxu151(tt(),PeRCenTX) -> axxu152(axxisLNat(PeRCenTX)) || 12: axxu152(tt()) -> tt() || 13: axxu161(tt(),PeRCenTX) -> cons(mark(PeRCenTX),natsFrom(s(PeRCenTX))) || 14: axxu171(tt(),PeRCenTX,PeRCenTY) -> axxu172(axxisLNat(PeRCenTY),PeRCenTX,PeRCenTY) || 15: axxu172(tt(),PeRCenTX,PeRCenTY) -> axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY))) || 16: axxu181(tt(),PeRCenTX) -> axxu182(axxisLNat(PeRCenTX),PeRCenTX) || 17: axxu182(tt(),PeRCenTX) -> mark(PeRCenTX) || 18: axxu191(tt(),PeRCenTX) -> pair(nil(),mark(PeRCenTX)) || 19: axxu201(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu202(axxisNatural(PeRCenTY),PeRCenTX,PeRCenTY,PeRCenTZ) || 20: axxu202(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu203(axxisLNat(PeRCenTZ),PeRCenTX,PeRCenTY,PeRCenTZ) || 21: axxu203(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> axxu204(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY) || 22: axxu204(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> pair(cons(mark(PeRCenTZ),PeRCenTX),mark(PeRCenTY)) || 23: axxu21(tt(),PeRCenTX,PeRCenTY) -> axxu22(axxisLNat(PeRCenTY),PeRCenTX) || 24: axxu211(tt(),PeRCenTX) -> axxu212(axxisLNat(PeRCenTX),PeRCenTX) || 25: axxu212(tt(),PeRCenTX) -> mark(PeRCenTX) || 26: axxu22(tt(),PeRCenTX) -> mark(PeRCenTX) || 27: axxu221(tt(),PeRCenTX,PeRCenTY) -> axxu222(axxisLNat(PeRCenTY),PeRCenTX,PeRCenTY) || 28: axxu222(tt(),PeRCenTX,PeRCenTY) -> axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))) || 29: axxu31(tt(),PeRCenTX,PeRCenTY) -> axxu32(axxisLNat(PeRCenTY),PeRCenTX) || 30: axxu32(tt(),PeRCenTX) -> mark(PeRCenTX) || 31: axxu41(tt(),PeRCenTX) -> axxu42(axxisLNat(PeRCenTX)) || 32: axxu42(tt()) -> tt() || 33: axxu51(tt(),PeRCenTX) -> axxu52(axxisLNat(PeRCenTX)) || 34: axxu52(tt()) -> tt() || 35: axxu61(tt()) -> tt() || 36: axxu71(tt()) -> tt() || 37: axxu81(tt()) -> tt() || 38: axxu91(tt()) -> tt() || 39: axxafterNth(PeRCenTX,PeRCenTY) -> axxu11(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || 40: axxfst(pair(PeRCenTX,PeRCenTY)) -> axxu21(axxisLNat(PeRCenTX),PeRCenTX,PeRCenTY) || 41: axxhead(cons(PeRCenTX,PeRCenTY)) -> axxu31(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || 42: axxisLNat(nil()) -> tt() || 43: axxisLNat(afterNth(PeRCenTX,PeRCenTY)) -> axxu41(axxisNatural(PeRCenTX),PeRCenTY) || 44: axxisLNat(cons(PeRCenTX,PeRCenTY)) -> axxu51(axxisNatural(PeRCenTX),PeRCenTY) || 45: axxisLNat(fst(PeRCenTX)) -> axxu61(axxisPLNat(PeRCenTX)) || 46: axxisLNat(natsFrom(PeRCenTX)) -> axxu71(axxisNatural(PeRCenTX)) || 47: axxisLNat(snd(PeRCenTX)) -> axxu81(axxisPLNat(PeRCenTX)) || 48: axxisLNat(tail(PeRCenTX)) -> axxu91(axxisLNat(PeRCenTX)) || 49: axxisLNat(take(PeRCenTX,PeRCenTY)) -> axxu101(axxisNatural(PeRCenTX),PeRCenTY) || 50: axxisNatural(0()) -> tt() || 51: axxisNatural(head(PeRCenTX)) -> axxu111(axxisLNat(PeRCenTX)) || 52: axxisNatural(s(PeRCenTX)) -> axxu121(axxisNatural(PeRCenTX)) || 53: axxisNatural(sel(PeRCenTX,PeRCenTY)) -> axxu131(axxisNatural(PeRCenTX),PeRCenTY) || 54: axxisPLNat(pair(PeRCenTX,PeRCenTY)) -> axxu141(axxisLNat(PeRCenTX),PeRCenTY) || 55: axxisPLNat(splitAt(PeRCenTX,PeRCenTY)) -> axxu151(axxisNatural(PeRCenTX),PeRCenTY) || 56: axxnatsFrom(PeRCenTX) -> axxu161(axxisNatural(PeRCenTX),PeRCenTX) || 57: axxsel(PeRCenTX,PeRCenTY) -> axxu171(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || 58: axxsnd(pair(PeRCenTX,PeRCenTY)) -> axxu181(axxisLNat(PeRCenTX),PeRCenTY) || 59: axxsplitAt(0(),PeRCenTX) -> axxu191(axxisLNat(PeRCenTX),PeRCenTX) || 60: axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> axxu201(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY,PeRCenTZ) || 61: axxtail(cons(PeRCenTX,PeRCenTY)) -> axxu211(axxisNatural(PeRCenTX),PeRCenTY) || 62: axxtake(PeRCenTX,PeRCenTY) -> axxu221(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || 63: mark(u101(PeRCenTX,PeRCenTY)) -> axxu101(mark(PeRCenTX),PeRCenTY) || 64: mark(u102(PeRCenTX)) -> axxu102(mark(PeRCenTX)) || 65: mark(isLNat(PeRCenTX)) -> axxisLNat(PeRCenTX) || 66: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 67: mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu12(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 68: mark(u111(PeRCenTX)) -> axxu111(mark(PeRCenTX)) || 69: mark(snd(PeRCenTX)) -> axxsnd(mark(PeRCenTX)) || 70: mark(splitAt(PeRCenTX,PeRCenTY)) -> axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)) || 71: mark(u121(PeRCenTX)) -> axxu121(mark(PeRCenTX)) || 72: mark(u131(PeRCenTX,PeRCenTY)) -> axxu131(mark(PeRCenTX),PeRCenTY) || 73: mark(u132(PeRCenTX)) -> axxu132(mark(PeRCenTX)) || 74: mark(u141(PeRCenTX,PeRCenTY)) -> axxu141(mark(PeRCenTX),PeRCenTY) || 75: mark(u142(PeRCenTX)) -> axxu142(mark(PeRCenTX)) || 76: mark(u151(PeRCenTX,PeRCenTY)) -> axxu151(mark(PeRCenTX),PeRCenTY) || 77: mark(u152(PeRCenTX)) -> axxu152(mark(PeRCenTX)) || 78: mark(u161(PeRCenTX,PeRCenTY)) -> axxu161(mark(PeRCenTX),PeRCenTY) || 79: mark(natsFrom(PeRCenTX)) -> axxnatsFrom(mark(PeRCenTX)) || 80: mark(u171(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu171(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 81: mark(u172(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu172(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 82: mark(head(PeRCenTX)) -> axxhead(mark(PeRCenTX)) || 83: mark(afterNth(PeRCenTX,PeRCenTY)) -> axxafterNth(mark(PeRCenTX),mark(PeRCenTY)) || 84: mark(u181(PeRCenTX,PeRCenTY)) -> axxu181(mark(PeRCenTX),PeRCenTY) || 85: mark(u182(PeRCenTX,PeRCenTY)) -> axxu182(mark(PeRCenTX),PeRCenTY) || 86: mark(u191(PeRCenTX,PeRCenTY)) -> axxu191(mark(PeRCenTX),PeRCenTY) || 87: mark(u201(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu201(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || 88: mark(u202(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu202(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || 89: mark(isNatural(PeRCenTX)) -> axxisNatural(PeRCenTX) || 90: mark(u203(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> axxu203(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || 91: mark(u204(PeRCenTX,PeRCenTY)) -> axxu204(mark(PeRCenTX),PeRCenTY) || 92: mark(u21(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu21(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 93: mark(u22(PeRCenTX,PeRCenTY)) -> axxu22(mark(PeRCenTX),PeRCenTY) || 94: mark(u211(PeRCenTX,PeRCenTY)) -> axxu211(mark(PeRCenTX),PeRCenTY) || 95: mark(u212(PeRCenTX,PeRCenTY)) -> axxu212(mark(PeRCenTX),PeRCenTY) || 96: mark(u221(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu221(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 97: mark(u222(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu222(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 98: mark(fst(PeRCenTX)) -> axxfst(mark(PeRCenTX)) || 99: mark(u31(PeRCenTX,PeRCenTY,PeRCenTZ)) -> axxu31(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || 100: mark(u32(PeRCenTX,PeRCenTY)) -> axxu32(mark(PeRCenTX),PeRCenTY) || 101: mark(u41(PeRCenTX,PeRCenTY)) -> axxu41(mark(PeRCenTX),PeRCenTY) || 102: mark(u42(PeRCenTX)) -> axxu42(mark(PeRCenTX)) || 103: mark(u51(PeRCenTX,PeRCenTY)) -> axxu51(mark(PeRCenTX),PeRCenTY) || 104: mark(u52(PeRCenTX)) -> axxu52(mark(PeRCenTX)) || 105: mark(u61(PeRCenTX)) -> axxu61(mark(PeRCenTX)) || 106: mark(u71(PeRCenTX)) -> axxu71(mark(PeRCenTX)) || 107: mark(u81(PeRCenTX)) -> axxu81(mark(PeRCenTX)) || 108: mark(u91(PeRCenTX)) -> axxu91(mark(PeRCenTX)) || 109: mark(isPLNat(PeRCenTX)) -> axxisPLNat(PeRCenTX) || 110: mark(tail(PeRCenTX)) -> axxtail(mark(PeRCenTX)) || 111: mark(take(PeRCenTX,PeRCenTY)) -> axxtake(mark(PeRCenTX),mark(PeRCenTY)) || 112: mark(sel(PeRCenTX,PeRCenTY)) -> axxsel(mark(PeRCenTX),mark(PeRCenTY)) || 113: mark(tt()) -> tt() || 114: mark(cons(PeRCenTX,PeRCenTY)) -> cons(mark(PeRCenTX),PeRCenTY) || 115: mark(s(PeRCenTX)) -> s(mark(PeRCenTX)) || 116: mark(pair(PeRCenTX,PeRCenTY)) -> pair(mark(PeRCenTX),mark(PeRCenTY)) || 117: mark(nil()) -> nil() || 118: mark(0()) -> 0() || 119: axxu101(PeRCenTX,PeRCenTY) -> u101(PeRCenTX,PeRCenTY) || 120: axxu102(PeRCenTX) -> u102(PeRCenTX) || 121: axxisLNat(PeRCenTX) -> isLNat(PeRCenTX) || 122: axxu11(PeRCenTX,PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 123: axxu12(PeRCenTX,PeRCenTY,PeRCenTZ) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 124: axxu111(PeRCenTX) -> u111(PeRCenTX) || 125: axxsnd(PeRCenTX) -> snd(PeRCenTX) || 126: axxsplitAt(PeRCenTX,PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY) || 127: axxu121(PeRCenTX) -> u121(PeRCenTX) || 128: axxu131(PeRCenTX,PeRCenTY) -> u131(PeRCenTX,PeRCenTY) || 129: axxu132(PeRCenTX) -> u132(PeRCenTX) || 130: axxu141(PeRCenTX,PeRCenTY) -> u141(PeRCenTX,PeRCenTY) || 131: axxu142(PeRCenTX) -> u142(PeRCenTX) || 132: axxu151(PeRCenTX,PeRCenTY) -> u151(PeRCenTX,PeRCenTY) || 133: axxu152(PeRCenTX) -> u152(PeRCenTX) || 134: axxu161(PeRCenTX,PeRCenTY) -> u161(PeRCenTX,PeRCenTY) || 135: axxnatsFrom(PeRCenTX) -> natsFrom(PeRCenTX) || 136: axxu171(PeRCenTX,PeRCenTY,PeRCenTZ) -> u171(PeRCenTX,PeRCenTY,PeRCenTZ) || 137: axxu172(PeRCenTX,PeRCenTY,PeRCenTZ) -> u172(PeRCenTX,PeRCenTY,PeRCenTZ) || 138: axxhead(PeRCenTX) -> head(PeRCenTX) || 139: axxafterNth(PeRCenTX,PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY) || 140: axxu181(PeRCenTX,PeRCenTY) -> u181(PeRCenTX,PeRCenTY) || 141: axxu182(PeRCenTX,PeRCenTY) -> u182(PeRCenTX,PeRCenTY) || 142: axxu191(PeRCenTX,PeRCenTY) -> u191(PeRCenTX,PeRCenTY) || 143: axxu201(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u201(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 144: axxu202(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u202(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 145: axxisNatural(PeRCenTX) -> isNatural(PeRCenTX) || 146: axxu203(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) -> u203(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 147: axxu204(PeRCenTX,PeRCenTY) -> u204(PeRCenTX,PeRCenTY) || 148: axxu21(PeRCenTX,PeRCenTY,PeRCenTZ) -> u21(PeRCenTX,PeRCenTY,PeRCenTZ) || 149: axxu22(PeRCenTX,PeRCenTY) -> u22(PeRCenTX,PeRCenTY) || 150: axxu211(PeRCenTX,PeRCenTY) -> u211(PeRCenTX,PeRCenTY) || 151: axxu212(PeRCenTX,PeRCenTY) -> u212(PeRCenTX,PeRCenTY) || 152: axxu221(PeRCenTX,PeRCenTY,PeRCenTZ) -> u221(PeRCenTX,PeRCenTY,PeRCenTZ) || 153: axxu222(PeRCenTX,PeRCenTY,PeRCenTZ) -> u222(PeRCenTX,PeRCenTY,PeRCenTZ) || 154: axxfst(PeRCenTX) -> fst(PeRCenTX) || 155: axxu31(PeRCenTX,PeRCenTY,PeRCenTZ) -> u31(PeRCenTX,PeRCenTY,PeRCenTZ) || 156: axxu32(PeRCenTX,PeRCenTY) -> u32(PeRCenTX,PeRCenTY) || 157: axxu41(PeRCenTX,PeRCenTY) -> u41(PeRCenTX,PeRCenTY) || 158: axxu42(PeRCenTX) -> u42(PeRCenTX) || 159: axxu51(PeRCenTX,PeRCenTY) -> u51(PeRCenTX,PeRCenTY) || 160: axxu52(PeRCenTX) -> u52(PeRCenTX) || 161: axxu61(PeRCenTX) -> u61(PeRCenTX) || 162: axxu71(PeRCenTX) -> u71(PeRCenTX) || 163: axxu81(PeRCenTX) -> u81(PeRCenTX) || 164: axxu91(PeRCenTX) -> u91(PeRCenTX) || 165: axxisPLNat(PeRCenTX) -> isPLNat(PeRCenTX) || 166: axxtail(PeRCenTX) -> tail(PeRCenTX) || 167: axxtake(PeRCenTX,PeRCenTY) -> take(PeRCenTX,PeRCenTY) || 168: axxsel(PeRCenTX,PeRCenTY) -> sel(PeRCenTX,PeRCenTY) || 169: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX || 170: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY || Number of strict rules: 170 || Direct POLO(bPol) ... failed. || Uncurrying ... failed. || Dependency Pairs: || #1: #mark(u191(PeRCenTX,PeRCenTY)) -> #axxu191(mark(PeRCenTX),PeRCenTY) || #2: #mark(u191(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #3: #axxisLNat(afterNth(PeRCenTX,PeRCenTY)) -> #axxu41(axxisNatural(PeRCenTX),PeRCenTY) || #4: #axxisLNat(afterNth(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #5: #axxu31(tt(),PeRCenTX,PeRCenTY) -> #axxu32(axxisLNat(PeRCenTY),PeRCenTX) || #6: #axxu31(tt(),PeRCenTX,PeRCenTY) -> #axxisLNat(PeRCenTY) || #7: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY)) || #8: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #9: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #10: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #11: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #12: #axxisLNat(natsFrom(PeRCenTX)) -> #axxu71(axxisNatural(PeRCenTX)) || #13: #axxisLNat(natsFrom(PeRCenTX)) -> #axxisNatural(PeRCenTX) || #14: #mark(s(PeRCenTX)) -> #mark(PeRCenTX) || #15: #mark(u212(PeRCenTX,PeRCenTY)) -> #axxu212(mark(PeRCenTX),PeRCenTY) || #16: #mark(u212(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #17: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #axxu31(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || #18: #axxhead(cons(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #19: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #20: #mark(u31(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu31(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #21: #mark(u31(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #22: #mark(u222(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu222(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #23: #mark(u222(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #24: #mark(u204(PeRCenTX,PeRCenTY)) -> #axxu204(mark(PeRCenTX),PeRCenTY) || #25: #mark(u204(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #26: #mark(u132(PeRCenTX)) -> #axxu132(mark(PeRCenTX)) || #27: #mark(u132(PeRCenTX)) -> #mark(PeRCenTX) || #28: #axxisLNat(snd(PeRCenTX)) -> #axxu81(axxisPLNat(PeRCenTX)) || #29: #axxisLNat(snd(PeRCenTX)) -> #axxisPLNat(PeRCenTX) || #30: #axxisNatural(sel(PeRCenTX,PeRCenTY)) -> #axxu131(axxisNatural(PeRCenTX),PeRCenTY) || #31: #axxisNatural(sel(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #32: #mark(u121(PeRCenTX)) -> #axxu121(mark(PeRCenTX)) || #33: #mark(u121(PeRCenTX)) -> #mark(PeRCenTX) || #34: #axxisLNat(tail(PeRCenTX)) -> #axxu91(axxisLNat(PeRCenTX)) || #35: #axxisLNat(tail(PeRCenTX)) -> #axxisLNat(PeRCenTX) || #36: #mark(u142(PeRCenTX)) -> #axxu142(mark(PeRCenTX)) || #37: #mark(u142(PeRCenTX)) -> #mark(PeRCenTX) || #38: #mark(sel(PeRCenTX,PeRCenTY)) -> #axxsel(mark(PeRCenTX),mark(PeRCenTY)) || #39: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #40: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #41: #mark(u141(PeRCenTX,PeRCenTY)) -> #axxu141(mark(PeRCenTX),PeRCenTY) || #42: #mark(u141(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #43: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #axxu181(axxisLNat(PeRCenTX),PeRCenTY) || #44: #axxsnd(pair(PeRCenTX,PeRCenTY)) -> #axxisLNat(PeRCenTX) || #45: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #axxu211(axxisNatural(PeRCenTX),PeRCenTY) || #46: #axxtail(cons(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #47: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #48: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #49: #axxsplitAt(0(),PeRCenTX) -> #axxu191(axxisLNat(PeRCenTX),PeRCenTX) || #50: #axxsplitAt(0(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #51: #mark(tail(PeRCenTX)) -> #axxtail(mark(PeRCenTX)) || #52: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX) || #53: #axxisPLNat(splitAt(PeRCenTX,PeRCenTY)) -> #axxu151(axxisNatural(PeRCenTX),PeRCenTY) || #54: #axxisPLNat(splitAt(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #55: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu12(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #56: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #57: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #axxu21(axxisLNat(PeRCenTX),PeRCenTX,PeRCenTY) || #58: #axxfst(pair(PeRCenTX,PeRCenTY)) -> #axxisLNat(PeRCenTX) || #59: #mark(u203(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu203(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || #60: #mark(u203(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX) || #61: #mark(u81(PeRCenTX)) -> #axxu81(mark(PeRCenTX)) || #62: #mark(u81(PeRCenTX)) -> #mark(PeRCenTX) || #63: #axxisNatural(head(PeRCenTX)) -> #axxu111(axxisLNat(PeRCenTX)) || #64: #axxisNatural(head(PeRCenTX)) -> #axxisLNat(PeRCenTX) || #65: #axxu161(tt(),PeRCenTX) -> #mark(PeRCenTX) || #66: #axxu141(tt(),PeRCenTX) -> #axxu142(axxisLNat(PeRCenTX)) || #67: #axxu141(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #68: #axxu151(tt(),PeRCenTX) -> #axxu152(axxisLNat(PeRCenTX)) || #69: #axxu151(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #70: #mark(fst(PeRCenTX)) -> #axxfst(mark(PeRCenTX)) || #71: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX) || #72: #axxsel(PeRCenTX,PeRCenTY) -> #axxu171(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || #73: #axxsel(PeRCenTX,PeRCenTY) -> #axxisNatural(PeRCenTX) || #74: #mark(u151(PeRCenTX,PeRCenTY)) -> #axxu151(mark(PeRCenTX),PeRCenTY) || #75: #mark(u151(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #76: #mark(isPLNat(PeRCenTX)) -> #axxisPLNat(PeRCenTX) || #77: #mark(u211(PeRCenTX,PeRCenTY)) -> #axxu211(mark(PeRCenTX),PeRCenTY) || #78: #mark(u211(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #79: #axxu211(tt(),PeRCenTX) -> #axxu212(axxisLNat(PeRCenTX),PeRCenTX) || #80: #axxu211(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #81: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)) || #82: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #83: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #84: #axxu21(tt(),PeRCenTX,PeRCenTY) -> #axxu22(axxisLNat(PeRCenTY),PeRCenTX) || #85: #axxu21(tt(),PeRCenTX,PeRCenTY) -> #axxisLNat(PeRCenTY) || #86: #mark(u172(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu172(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #87: #mark(u172(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #88: #mark(u161(PeRCenTX,PeRCenTY)) -> #axxu161(mark(PeRCenTX),PeRCenTY) || #89: #mark(u161(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #90: #axxisLNat(fst(PeRCenTX)) -> #axxu61(axxisPLNat(PeRCenTX)) || #91: #axxisLNat(fst(PeRCenTX)) -> #axxisPLNat(PeRCenTX) || #92: #mark(u221(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu221(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #93: #mark(u221(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #94: #mark(snd(PeRCenTX)) -> #axxsnd(mark(PeRCenTX)) || #95: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX) || #96: #mark(u41(PeRCenTX,PeRCenTY)) -> #axxu41(mark(PeRCenTX),PeRCenTY) || #97: #mark(u41(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #98: #axxu41(tt(),PeRCenTX) -> #axxu42(axxisLNat(PeRCenTX)) || #99: #axxu41(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #100: #mark(natsFrom(PeRCenTX)) -> #axxnatsFrom(mark(PeRCenTX)) || #101: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX) || #102: #axxnatsFrom(PeRCenTX) -> #axxu161(axxisNatural(PeRCenTX),PeRCenTX) || #103: #axxnatsFrom(PeRCenTX) -> #axxisNatural(PeRCenTX) || #104: #mark(isNatural(PeRCenTX)) -> #axxisNatural(PeRCenTX) || #105: #mark(head(PeRCenTX)) -> #axxhead(mark(PeRCenTX)) || #106: #mark(head(PeRCenTX)) -> #mark(PeRCenTX) || #107: #mark(take(PeRCenTX,PeRCenTY)) -> #axxtake(mark(PeRCenTX),mark(PeRCenTY)) || #108: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #109: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #110: #axxu171(tt(),PeRCenTX,PeRCenTY) -> #axxu172(axxisLNat(PeRCenTY),PeRCenTX,PeRCenTY) || #111: #axxu171(tt(),PeRCenTX,PeRCenTY) -> #axxisLNat(PeRCenTY) || #112: #mark(u71(PeRCenTX)) -> #axxu71(mark(PeRCenTX)) || #113: #mark(u71(PeRCenTX)) -> #mark(PeRCenTX) || #114: #axxtake(PeRCenTX,PeRCenTY) -> #axxu221(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || #115: #axxtake(PeRCenTX,PeRCenTY) -> #axxisNatural(PeRCenTX) || #116: #axxu32(tt(),PeRCenTX) -> #mark(PeRCenTX) || #117: #axxisNatural(s(PeRCenTX)) -> #axxu121(axxisNatural(PeRCenTX)) || #118: #axxisNatural(s(PeRCenTX)) -> #axxisNatural(PeRCenTX) || #119: #axxisLNat(take(PeRCenTX,PeRCenTY)) -> #axxu101(axxisNatural(PeRCenTX),PeRCenTY) || #120: #axxisLNat(take(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #121: #axxu212(tt(),PeRCenTX) -> #mark(PeRCenTX) || #122: #mark(u91(PeRCenTX)) -> #axxu91(mark(PeRCenTX)) || #123: #mark(u91(PeRCenTX)) -> #mark(PeRCenTX) || #124: #axxu202(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu203(axxisLNat(PeRCenTZ),PeRCenTX,PeRCenTY,PeRCenTZ) || #125: #axxu202(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxisLNat(PeRCenTZ) || #126: #mark(u202(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu202(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || #127: #mark(u202(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX) || #128: #axxu131(tt(),PeRCenTX) -> #axxu132(axxisLNat(PeRCenTX)) || #129: #axxu131(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #130: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxu11(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY) || #131: #axxafterNth(PeRCenTX,PeRCenTY) -> #axxisNatural(PeRCenTX) || #132: #mark(u21(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu21(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #133: #mark(u21(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #134: #mark(u22(PeRCenTX,PeRCenTY)) -> #axxu22(mark(PeRCenTX),PeRCenTY) || #135: #mark(u22(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #136: #mark(u102(PeRCenTX)) -> #axxu102(mark(PeRCenTX)) || #137: #mark(u102(PeRCenTX)) -> #mark(PeRCenTX) || #138: #axxu51(tt(),PeRCenTX) -> #axxu52(axxisLNat(PeRCenTX)) || #139: #axxu51(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #140: #mark(u131(PeRCenTX,PeRCenTY)) -> #axxu131(mark(PeRCenTX),PeRCenTY) || #141: #mark(u131(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #142: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #axxsnd(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))) || #143: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)) || #144: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX) || #145: #axxu12(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY) || #146: #axxisLNat(cons(PeRCenTX,PeRCenTY)) -> #axxu51(axxisNatural(PeRCenTX),PeRCenTY) || #147: #axxisLNat(cons(PeRCenTX,PeRCenTY)) -> #axxisNatural(PeRCenTX) || #148: #mark(isLNat(PeRCenTX)) -> #axxisLNat(PeRCenTX) || #149: #axxu222(tt(),PeRCenTX,PeRCenTY) -> #axxfst(axxsplitAt(mark(PeRCenTX),mark(PeRCenTY))) || #150: #axxu222(tt(),PeRCenTX,PeRCenTY) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTY)) || #151: #axxu222(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX) || #152: #axxu222(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY) || #153: #axxu204(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTZ) || #154: #axxu204(pair(PeRCenTX,PeRCenTY),PeRCenTZ) -> #mark(PeRCenTY) || #155: #mark(u181(PeRCenTX,PeRCenTY)) -> #axxu181(mark(PeRCenTX),PeRCenTY) || #156: #mark(u181(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #157: #mark(u201(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #axxu201(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || #158: #mark(u201(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX) || #159: #axxu221(tt(),PeRCenTX,PeRCenTY) -> #axxu222(axxisLNat(PeRCenTY),PeRCenTX,PeRCenTY) || #160: #axxu221(tt(),PeRCenTX,PeRCenTY) -> #axxisLNat(PeRCenTY) || #161: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxu201(axxisNatural(PeRCenTX),PeRCenTX,PeRCenTY,PeRCenTZ) || #162: #axxsplitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ)) -> #axxisNatural(PeRCenTX) || #163: #axxu182(tt(),PeRCenTX) -> #mark(PeRCenTX) || #164: #axxu201(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu202(axxisNatural(PeRCenTY),PeRCenTX,PeRCenTY,PeRCenTZ) || #165: #axxu201(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxisNatural(PeRCenTY) || #166: #mark(u101(PeRCenTX,PeRCenTY)) -> #axxu101(mark(PeRCenTX),PeRCenTY) || #167: #mark(u101(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #168: #mark(u61(PeRCenTX)) -> #axxu61(mark(PeRCenTX)) || #169: #mark(u61(PeRCenTX)) -> #mark(PeRCenTX) || #170: #axxu22(tt(),PeRCenTX) -> #mark(PeRCenTX) || #171: #mark(u32(PeRCenTX,PeRCenTY)) -> #axxu32(mark(PeRCenTX),PeRCenTY) || #172: #mark(u32(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #173: #mark(u182(PeRCenTX,PeRCenTY)) -> #axxu182(mark(PeRCenTX),PeRCenTY) || #174: #mark(u182(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #175: #mark(u111(PeRCenTX)) -> #axxu111(mark(PeRCenTX)) || #176: #mark(u111(PeRCenTX)) -> #mark(PeRCenTX) || #177: #axxu203(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxu204(axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)),PeRCenTY) || #178: #axxu203(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #axxsplitAt(mark(PeRCenTX),mark(PeRCenTZ)) || #179: #axxu203(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTX) || #180: #axxu203(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) -> #mark(PeRCenTZ) || #181: #axxu181(tt(),PeRCenTX) -> #axxu182(axxisLNat(PeRCenTX),PeRCenTX) || #182: #axxu181(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #183: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #axxu12(axxisLNat(PeRCenTY),PeRCenTX,PeRCenTY) || #184: #axxu11(tt(),PeRCenTX,PeRCenTY) -> #axxisLNat(PeRCenTY) || #185: #mark(u152(PeRCenTX)) -> #axxu152(mark(PeRCenTX)) || #186: #mark(u152(PeRCenTX)) -> #mark(PeRCenTX) || #187: #axxu101(tt(),PeRCenTX) -> #axxu102(axxisLNat(PeRCenTX)) || #188: #axxu101(tt(),PeRCenTX) -> #axxisLNat(PeRCenTX) || #189: #axxisPLNat(pair(PeRCenTX,PeRCenTY)) -> #axxu141(axxisLNat(PeRCenTX),PeRCenTY) || #190: #axxisPLNat(pair(PeRCenTX,PeRCenTY)) -> #axxisLNat(PeRCenTX) || #191: #axxu172(tt(),PeRCenTX,PeRCenTY) -> #axxhead(axxafterNth(mark(PeRCenTX),mark(PeRCenTY))) || #192: #axxu172(tt(),PeRCenTX,PeRCenTY) -> #axxafterNth(mark(PeRCenTX),mark(PeRCenTY)) || #193: #axxu172(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTX) || #194: #axxu172(tt(),PeRCenTX,PeRCenTY) -> #mark(PeRCenTY) || #195: #mark(u42(PeRCenTX)) -> #axxu42(mark(PeRCenTX)) || #196: #mark(u42(PeRCenTX)) -> #mark(PeRCenTX) || #197: #mark(u51(PeRCenTX,PeRCenTY)) -> #axxu51(mark(PeRCenTX),PeRCenTY) || #198: #mark(u51(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #199: #mark(u52(PeRCenTX)) -> #axxu52(mark(PeRCenTX)) || #200: #mark(u52(PeRCenTX)) -> #mark(PeRCenTX) || #201: #mark(u171(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #axxu171(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #202: #mark(u171(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #203: #axxu191(tt(),PeRCenTX) -> #mark(PeRCenTX) || Number of SCCs: 2, DPs: 151 || SCC { #3 #4 #13 #29..31 #35 #53 #54 #64 #67 #69 #91 #99 #118..120 #129 #139 #146 #147 #188..190 } || POLO(Sum)... succeeded. || #axxu172 w: 0 || u81 w: 0 || #axxu51 w: x1 + x2 || u172 w: 0 || #axxu32 w: 0 || TIlDePAIR w: 0 || #axxu141 w: x1 + x2 || axxu211 w: 0 || axxu142 w: x1 || s w: x1 + 1 || axxisLNat w: x1 + 1 || u132 w: 0 || #axxu12 w: 0 || axxu121 w: x1 || u91 w: 0 || #axxu111 w: 0 || u111 w: 0 || #axxu211 w: 0 || #axxu132 w: 0 || axxu131 w: x1 + x2 || u191 w: 0 || isPLNat w: 0 || axxsnd w: 0 || u102 w: 0 || axxu191 w: 0 || axxu11 w: 0 || u121 w: 0 || axxu172 w: 0 || axxu32 w: 0 || #axxu102 w: 0 || #axxu181 w: 0 || #axxu101 w: x1 + x2 || u181 w: 0 || #axxisLNat w: x1 || axxu132 w: x1 || take w: x1 + x2 + 2 || #axxu204 w: 0 || axxsplitAt w: 0 || #axxu221 w: 0 || #axxu222 w: 0 || pair w: x1 + x2 + 2 || axxu91 w: x1 || fst w: x1 + 1 || u222 w: 0 || #axxu151 w: x1 + x2 || u131 w: 0 || natsFrom w: x1 + 1 || u182 w: 0 || u212 w: 0 || splitAt w: x1 + x2 + 2 || u52 w: 0 || #axxu11 w: 0 || axxu201 w: 0 || axxu102 w: x1 || u61 w: 0 || axxu31 w: 0 || axxu203 w: 0 || u221 w: 0 || u151 w: 0 || axxu22 w: 0 || u202 w: 0 || isNatural w: 0 || #axxu121 w: 0 || #axxsplitAt w: 0 || axxnatsFrom w: 0 || u41 w: 0 || axxisNatural w: x1 + 1 || u211 w: 0 || axxu151 w: x1 + x2 || axxu181 w: 0 || #axxu91 w: 0 || #axxu201 w: 0 || tail w: x1 + 1 || u51 w: 0 || #axxafterNth w: 0 || #mark w: 0 || #axxtail w: 0 || 0 w: 1 || axxu141 w: x1 + x2 || #axxnatsFrom w: 0 || axxu81 w: x1 || axxisPLNat w: x1 + 1 || #axxisPLNat w: x1 || axxu152 w: x1 || axxu182 w: 0 || u11 w: 0 || axxu204 w: 0 || sel w: x1 + x2 + 2 || u32 w: 0 || afterNth w: x1 + x2 + 2 || #axxu212 w: 0 || #axxu161 w: 0 || nil w: 1 || #axxsnd w: 0 || isLNat w: 0 || #TIlDePAIR w: 0 || #axxu21 w: 0 || axxu41 w: x1 + x2 || #axxu142 w: 0 || #axxu202 w: 0 || axxafterNth w: 0 || mark w: 0 || u12 w: 0 || #axxu152 w: 0 || u203 w: 0 || #axxu22 w: 0 || axxu71 w: x1 || u101 w: 0 || #axxu81 w: 0 || axxsel w: 0 || u201 w: 0 || u21 w: 0 || axxu52 w: x1 || #axxu52 w: 0 || axxu111 w: x1 || axxfst w: 0 || axxu61 w: x1 || axxu171 w: 0 || u161 w: 0 || #axxu31 w: 0 || u204 w: 0 || #axxsel w: 0 || #axxu42 w: 0 || axxu51 w: x1 + x2 || u171 w: 0 || axxu221 w: 0 || head w: x1 + 1 || cons w: x1 + x2 + 2 || u142 w: 0 || axxu222 w: 0 || snd w: x1 + 1 || #axxu41 w: x1 + x2 || u22 w: 0 || axxu12 w: 0 || axxtail w: 0 || u42 w: 0 || tt w: 1 || #axxu191 w: 0 || axxu42 w: x1 || #axxu131 w: x1 + x2 || u152 w: 0 || axxu161 w: 0 || axxu202 w: 0 || u71 w: 0 || axxtake w: 0 || #axxu61 w: 0 || #axxfst w: 0 || #axxu171 w: 0 || axxu101 w: x1 + x2 || #axxu71 w: 0 || #axxisNatural w: x1 || axxu212 w: 0 || u31 w: 0 || u141 w: 0 || axxu21 w: 0 || #axxu182 w: 0 || #axxu203 w: 0 || #axxtake w: 0 || #axxhead w: 0 || axxhead w: 0 || USABLE RULES: { 1 2 4 6..12 31..38 42..55 119..121 124 127..133 145 157..165 } || Removed DPs: #3 #4 #13 #29..31 #35 #53 #54 #64 #67 #69 #91 #99 #118..120 #129 #139 #146 #147 #188..190 || Number of SCCs: 1, DPs: 127 || SCC { #1 #2 #5 #7..11 #14..17 #19..25 #27 #33 #37..40 #42 #43 #45 #47..49 #51 #52 #55..57 #59 #60 #62 #65 #70..72 #75 #77..79 #81..84 #86..89 #92..95 #97 #100..102 #105..110 #113 #114 #116 #121 #123 #124 #126 #127 #130 #132..135 #137 #141..145 #149..159 #161 #163 #164 #167 #169..174 #176..181 #183 #186 #191..194 #196 #198 #200..203 } || POLO(Sum)... POLO(max)... succeeded. || #axxu172 w: max(x2 + 105, x3 + 106) || u81 w: x1 + 1 || #axxu51 w: 0 || u172 w: max(x1 + 98, x2 + 109, x3 + 97) || #axxu32 w: max(x1 + 9, x2 + 11) || TIlDePAIR w: 0 || #axxu141 w: 0 || axxu211 w: max(x1 + 8, x2 + 12) || axxu142 w: x1 + 1 || s w: x1 || axxisLNat w: x1 + 10 || u132 w: x1 + 2 || #axxu12 w: max(x2 + 57, x3 + 62) || axxu121 w: x1 || u91 w: x1 + 1 || #axxu111 w: 0 || u111 w: x1 + 1 || #axxu211 w: max(x2 + 18) || #axxu132 w: 0 || axxu131 w: max(x1 + 8, x2 + 121) || u191 w: max(x1 + 34, x2 + 21) || isPLNat w: x1 || axxsnd w: x1 + 3 || u102 w: x1 + 77 || axxu191 w: max(x1 + 34, x2 + 21) || axxu11 w: max(x1 + 74, x2 + 76, x3 + 72) || u121 w: x1 || axxu172 w: max(x1 + 98, x2 + 109, x3 + 97) || axxu32 w: max(x1 + 1, x2 + 12) || #axxu102 w: 0 || #axxu181 w: max(x2 + 24) || #axxu101 w: 0 || u181 w: max(x1 + 14, x2 + 15) || #axxisLNat w: 0 || axxu132 w: x1 + 2 || take w: max(x1 + 87, x2 + 79) || #axxu204 w: max(x1 + 1, x2 + 11) || axxsplitAt w: max(x1 + 48, x2 + 44) || #axxu221 w: max(x1 + 87, x2 + 73, x3 + 85) || #axxu222 w: max(x1 + 74, x2 + 72, x3 + 68) || pair w: max(x1 + 21, x2 + 21) || axxu91 w: x1 + 1 || fst w: x1 + 14 || u222 w: max(x1 + 65, x2 + 63, x3 + 63) || #axxu151 w: 0 || u131 w: max(x1 + 8, x2 + 121) || natsFrom w: x1 + 14 || u182 w: max(x1 + 4, x2 + 2) || u212 w: max(x1 + 2, x2 + 3) || splitAt w: max(x1 + 48, x2 + 44) || u52 w: x1 || #axxu11 w: max(x1 + 83, x2 + 85, x3 + 75) || axxu201 w: max(x1 + 40, x2 + 48, x3 + 53, x4 + 44) || axxu102 w: x1 + 77 || u61 w: x1 + 1 || axxu31 w: max(x1 + 8, x2 + 12, x3 + 11) || axxu203 w: max(x1 + 33, x2 + 48, x3 + 31, x4 + 44) || u221 w: max(x1 + 78, x2 + 75, x3 + 76) || u151 w: max(x1 + 37, x2 + 42) || axxu22 w: max(x1 + 11, x2 + 10) || u202 w: max(x1 + 45, x2 + 48, x3 + 43, x4 + 44) || isNatural w: x1 + 8 || #axxu121 w: 0 || #axxsplitAt w: max(x1 + 55, x2 + 50) || axxnatsFrom w: x1 + 14 || u41 w: max(x1 + 80, x2 + 87) || axxisNatural w: x1 + 8 || u211 w: max(x1 + 8, x2 + 12) || axxu151 w: max(x1 + 37, x2 + 42) || axxu181 w: max(x1 + 14, x2 + 15) || #axxu91 w: 0 || #axxu201 w: max(x1 + 47, x2 + 55, x3 + 59, x4 + 50) || tail w: x1 + 16 || u51 w: max(x1 + 11, x2 + 10) || #axxafterNth w: max(x1 + 92, x2 + 86) || #mark w: x1 + 10 || #axxtail w: x1 + 19 || 0 w: 1 || axxu141 w: max(x1 + 11, x2 + 11) || #axxnatsFrom w: x1 + 17 || axxu81 w: x1 + 1 || axxisPLNat w: x1 || #axxisPLNat w: 0 || axxu152 w: x1 + 32 || axxu182 w: max(x1 + 4, x2 + 2) || u11 w: max(x1 + 74, x2 + 76, x3 + 72) || axxu204 w: max(x1, x2 + 31) || sel w: max(x1 + 112, x2 + 114) || u32 w: max(x1 + 1, x2 + 12) || afterNth w: max(x1 + 83, x2 + 77) || #axxu212 w: max(x1 + 7, x2 + 12) || #axxu161 w: max(x1, x2 + 16) || nil w: 1 || #axxsnd w: x1 + 4 || isLNat w: x1 + 10 || #TIlDePAIR w: 0 || #axxu21 w: max(x1 + 33, x2 + 30, x3 + 18) || axxu41 w: max(x1 + 80, x2 + 87) || #axxu142 w: 0 || #axxu202 w: max(x2 + 55, x3 + 50, x4 + 50) || axxafterNth w: max(x1 + 83, x2 + 77) || mark w: x1 || u12 w: max(x1 + 47, x2 + 52, x3 + 53) || #axxu152 w: 0 || u203 w: max(x1 + 33, x2 + 48, x3 + 31, x4 + 44) || #axxu22 w: max(x1 + 7, x2 + 19) || axxu71 w: x1 + 1 || u101 w: max(x1 + 82, x2 + 89) || #axxu81 w: 0 || axxsel w: max(x1 + 112, x2 + 114) || u201 w: max(x1 + 40, x2 + 48, x3 + 53, x4 + 44) || u21 w: max(x1 + 25, x2 + 22, x3 + 21) || axxu52 w: x1 || #axxu52 w: 0 || axxu111 w: x1 + 1 || axxfst w: x1 + 14 || axxu61 w: x1 + 1 || axxu171 w: max(x1 + 104, x2 + 109, x3 + 110) || u161 w: max(x1 + 6, x2 + 14) || #axxu31 w: max(x1 + 14, x2 + 18, x3 + 20) || u204 w: max(x1, x2 + 31) || #axxsel w: max(x1 + 115, x2 + 123) || #axxu42 w: 0 || axxu51 w: max(x1 + 11, x2 + 10) || u171 w: max(x1 + 104, x2 + 109, x3 + 110) || axxu221 w: max(x1 + 78, x2 + 75, x3 + 76) || head w: x1 + 20 || cons w: max(x1 + 10, x2) || u142 w: x1 + 1 || axxu222 w: max(x1 + 65, x2 + 63, x3 + 63) || snd w: x1 + 3 || #axxu41 w: 0 || u22 w: max(x1 + 11, x2 + 10) || axxu12 w: max(x1 + 47, x2 + 52, x3 + 53) || axxtail w: x1 + 16 || u42 w: x1 + 77 || tt w: 4 || #axxu191 w: max(x1 + 7, x2 + 11) || axxu42 w: x1 + 77 || #axxu131 w: 0 || u152 w: x1 + 32 || axxu161 w: max(x1 + 6, x2 + 14) || axxu202 w: max(x1 + 45, x2 + 48, x3 + 43, x4 + 44) || u71 w: x1 + 1 || axxtake w: max(x1 + 87, x2 + 79) || #axxu61 w: 0 || #axxfst w: x1 + 23 || #axxu171 w: max(x2 + 106, x3 + 114) || axxu101 w: max(x1 + 82, x2 + 89) || #axxu71 w: 0 || #axxisNatural w: 0 || axxu212 w: max(x1 + 2, x2 + 3) || u31 w: max(x1 + 8, x2 + 12, x3 + 11) || u141 w: max(x1 + 11, x2 + 11) || axxu21 w: max(x1 + 25, x2 + 22, x3 + 21) || #axxu182 w: max(x1 + 13, x2 + 11) || #axxu203 w: max(x1 + 40, x2 + 55, x3 + 40, x4 + 50) || #axxtake w: max(x1 + 96, x2 + 86) || #axxhead w: x1 + 21 || axxhead w: x1 + 20 || USABLE RULES: { 1..168 } || Removed DPs: #1 #2 #5 #7..11 #15..17 #19..24 #27 #37..40 #42 #43 #45 #47..49 #51 #52 #55..57 #59 #60 #62 #65 #70..72 #75 #77..79 #81..84 #86..89 #92..95 #97 #100..102 #105..110 #113 #114 #116 #121 #123 #126 #127 #130 #132..135 #137 #141..145 #149..159 #163 #167 #169..174 #176 #177 #179..181 #183 #186 #191..194 #196 #198 #201..203 || Number of SCCs: 2, DPs: 8 || SCC { #14 #25 #33 #200 } || POLO(Sum)... succeeded. || #axxu172 w: 1 || u81 w: x1 + 10 || #axxu51 w: 0 || u172 w: x1 + x3 + 3 || #axxu32 w: 1 || TIlDePAIR w: 0 || #axxu141 w: 0 || axxu211 w: x1 + 2 || axxu142 w: 13 || s w: x1 + 1 || axxisLNat w: 11 || u132 w: x1 + 6 || #axxu12 w: 1 || axxu121 w: 11 || u91 w: x1 + 14 || #axxu111 w: 0 || u111 w: 6 || #axxu211 w: 1 || #axxu132 w: 0 || axxu131 w: x1 + x2 + 2 || u191 w: x1 + x2 + 11 || isPLNat w: x1 + 2 || axxsnd w: 4 || u102 w: 14 || axxu191 w: 10 || axxu11 w: x3 + 2 || u121 w: x1 + 12 || axxu172 w: x1 + x3 + 2 || axxu32 w: 13 || #axxu102 w: 0 || #axxu181 w: 0 || #axxu101 w: 0 || u181 w: x1 + x2 + 6 || #axxisLNat w: 0 || axxu132 w: x1 + 5 || take w: x2 + 1 || #axxu204 w: 2 || axxsplitAt w: 9 || #axxu221 w: 0 || #axxu222 w: 1 || pair w: x1 + x2 + 1 || axxu91 w: 13 || fst w: 1 || u222 w: x2 + x3 + 6 || #axxu151 w: 0 || u131 w: 3 || natsFrom w: x1 + 3 || u182 w: 7 || u212 w: 1 || splitAt w: x1 + 1 || u52 w: x1 + 6 || #axxu11 w: 1 || axxu201 w: x2 + x3 + x4 + 10 || axxu102 w: 13 || u61 w: 13 || axxu31 w: x1 || axxu203 w: x1 + x2 + x3 + x4 + 5 || u221 w: x2 + x3 + 1 || u151 w: 1 || axxu22 w: x2 + 13 || u202 w: x2 + 3 || isNatural w: 1 || #axxu121 w: 0 || #axxsplitAt w: 1 || axxnatsFrom w: 2 || u41 w: x2 + 1 || axxisNatural w: x1 + 9 || u211 w: x2 + 1 || axxu151 w: x1 + x2 || axxu181 w: 5 || #axxu91 w: 0 || #axxu201 w: 1 || tail w: 1 || u51 w: x2 + 1 || #axxafterNth w: 1 || #mark w: x1 + 1 || #axxtail w: 1 || 0 w: 1 || axxu141 w: x1 + 2 || #axxnatsFrom w: 1 || axxu81 w: x1 + 10 || axxisPLNat w: 1 || #axxisPLNat w: 0 || axxu152 w: x1 + 3 || axxu182 w: x2 + 6 || u11 w: x2 + 3 || axxu204 w: 19 || sel w: x1 + 1 || u32 w: 14 || afterNth w: 1 || #axxu212 w: 1 || #axxu161 w: 1 || nil w: 3 || #axxsnd w: 1 || isLNat w: 3 || #TIlDePAIR w: 0 || #axxu21 w: 1 || axxu41 w: x1 + 3 || #axxu142 w: 0 || #axxu202 w: 1 || axxafterNth w: x1 + x2 + 1 || mark w: x1 + 7 || u12 w: 4 || #axxu152 w: 0 || u203 w: 1 || #axxu22 w: 1 || axxu71 w: x1 + 3 || u101 w: 1 || #axxu81 w: 0 || axxsel w: 0 || u201 w: x3 + x4 + 1 || u21 w: x2 + x3 + 13 || axxu52 w: 13 || #axxu52 w: 0 || axxu111 w: 13 || axxfst w: x1 + 10 || axxu61 w: 12 || axxu171 w: x1 + 2 || u161 w: x2 + 3 || #axxu31 w: 1 || u204 w: x1 + x2 + 20 || #axxsel w: 1 || #axxu42 w: 0 || axxu51 w: x1 + x2 + 2 || u171 w: x1 + 1 || axxu221 w: x1 + 2 || head w: x1 + 4 || cons w: x1 + x2 + 5 || u142 w: 14 || axxu222 w: x1 + x2 + x3 + 5 || snd w: 1 || #axxu41 w: 0 || u22 w: x2 + 6 || axxu12 w: x2 + 3 || axxtail w: x1 + 6 || u42 w: 1 || tt w: 13 || #axxu191 w: 1 || axxu42 w: 8 || #axxu131 w: 0 || u152 w: 4 || axxu161 w: 2 || axxu202 w: x1 + x3 + 2 || u71 w: 2 || axxtake w: x1 + x2 + 1 || #axxu61 w: 0 || #axxfst w: 1 || #axxu171 w: 1 || axxu101 w: x1 + x2 + 3 || #axxu71 w: 0 || #axxisNatural w: 0 || axxu212 w: 6 || u31 w: x3 + 1 || u141 w: x2 + 1 || axxu21 w: 12 || #axxu182 w: 0 || #axxu203 w: 1 || #axxtake w: 1 || #axxhead w: 1 || axxhead w: x1 + 5 || USABLE RULES: { 10 36 } || Removed DPs: #14 #25 #33 #200 || Number of SCCs: 1, DPs: 4 || SCC { #124 #161 #164 #178 } || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded. || #axxu172 s: [2,3,1] p: 0 w: x1 + x2 + x3 + 1 || u81 s: [] p: 4 w: x1 + 1 || #axxu51 s: [] p: 0 w: max(x2 + 1) || u172 s: [] p: 0 w: max(x2 + 92, x3 + 90) || #axxu32 s: [] p: 0 w: x1 + 1 || TIlDePAIR s: [2,1] p: 0 w: x1 + x2 || #axxu141 s: [] p: 0 w: max(x2) || axxu211 s: [1] p: 13 w: max(x1 + 29, x2 + 2) || axxu142 s: [1] p: 3 w: x1 || s s: [1] p: 15 w: x1 || axxisLNat s: [] p: 12 w: x1 + 27 || u132 s: [] p: 14 w: x1 + 1 || #axxu12 s: [3,2,1] p: 0 w: x1 + x2 + x3 + 1 || axxu121 s: 1 || u91 s: [] p: 12 w: 55 || #axxu111 s: [] p: 0 w: 0 || u111 s: [] p: 12 w: 23 || #axxu211 s: [] p: 0 w: x1 || #axxu132 s: [] p: 0 w: 0 || axxu131 s: [] p: 9 w: x1 + x2 + 7 || u191 s: [2] p: 10 w: max(x2 + 12) || isPLNat s: [] p: 13 w: x1 + 26 || axxsnd s: [1] p: 3 w: x1 + 28 || u102 s: [] p: 14 w: x1 + 1 || axxu191 s: [2] p: 10 w: max(x2 + 12) || axxu11 s: [] p: 1 w: max(x2 + 62, x3 + 61) || u121 s: 1 || axxu172 s: [] p: 0 w: max(x2 + 92, x3 + 90) || axxu32 s: [] p: 7 w: max(x2 + 1) || #axxu102 s: [] p: 0 w: 0 || #axxu181 s: [] p: 0 w: x1 + 1 || #axxu101 s: [2] p: 0 w: x2 + 1 || u181 s: [] p: 4 w: max(x2 + 2) || #axxisLNat s: [] p: 0 w: 0 || axxu132 s: [] p: 14 w: x1 + 1 || take s: [] p: 13 w: x1 + x2 + 39 || #axxu204 s: [1,2] p: 0 w: x1 + x2 || axxsplitAt s: [1] p: 12 w: max(x1, x2 + 12) || #axxu221 s: [3,2,1] p: 0 w: x1 + x2 + x3 || #axxu222 s: [1] p: 0 w: x1 + x3 + 1 || pair s: [] p: 5 w: max(x1 + 8, x2 + 3) || axxu91 s: [] p: 12 w: 55 || fst s: [] p: 7 w: x1 + 24 || u222 s: [] p: 9 w: max(x2 + 38, x3 + 37) || #axxu151 s: [2,1] p: 0 w: max(x1 + 1, x2 + 1) || u131 s: [] p: 9 w: x1 + x2 + 7 || natsFrom s: [] p: 15 w: x1 + 14 || u182 s: [] p: 0 w: max(x2 + 1) || u212 s: [] p: 8 w: max(x2 + 1) || splitAt s: [1] p: 12 w: max(x1, x2 + 12) || u52 s: [] p: 14 w: 23 || #axxu11 s: [1] p: 0 w: x1 + x2 || axxu201 s: [1,4] p: 11 w: max(x1, x2, x3 + 24, x4 + 12) || axxu102 s: [] p: 14 w: x1 + 1 || u61 s: [] p: 12 w: 23 || axxu31 s: [] p: 12 w: max(x2 + 12, x3 + 28) || axxu203 s: [] p: 9 w: max(x2, x3 + 21, x4 + 12) || u221 s: [] p: 13 w: max(x2 + 38, x3 + 37) || u151 s: [] p: 12 w: max(x1 + 26, x2 + 28) || axxu22 s: [] p: 0 w: max(x2 + 4) || u202 s: [4] p: 10 w: max(x2, x3 + 23, x4 + 12) || isNatural s: [] p: 12 w: x1 || #axxu121 s: [] p: 0 w: 1 || #axxsplitAt s: [1] p: 12 w: max(x1) || axxnatsFrom s: [] p: 15 w: x1 + 14 || u41 s: [] p: 14 w: max(x2 + 61) || axxisNatural s: [] p: 12 w: x1 || u211 s: [1] p: 13 w: max(x1 + 29, x2 + 2) || axxu151 s: [] p: 12 w: max(x1 + 26, x2 + 28) || axxu181 s: [] p: 4 w: max(x2 + 2) || #axxu91 s: [] p: 0 w: 0 || #axxu201 s: [2] p: 12 w: max(x1, x2) || tail s: [1] p: 14 w: x1 + 28 || u51 s: [] p: 13 w: max(x2 + 24) || #axxafterNth s: [2] p: 0 w: x2 + 1 || #mark s: [] p: 0 w: 1 || #axxtail s: [] p: 0 w: 1 || 0 s: [] p: 0 w: 28 || axxu141 s: [] p: 4 w: max(x2 + 28) || #axxnatsFrom s: [] p: 0 w: 0 || axxu81 s: [] p: 4 w: x1 + 1 || axxisPLNat s: [] p: 13 w: x1 + 26 || #axxisPLNat s: [] p: 0 w: 0 || axxu152 s: [] p: 12 w: 23 || axxu182 s: [] p: 0 w: max(x2 + 1) || u11 s: [] p: 1 w: max(x2 + 62, x3 + 61) || axxu204 s: [] p: 5 w: max(x1, x2 + 21) || sel s: [1] p: 13 w: x1 + x2 + 95 || u32 s: [] p: 7 w: max(x2 + 1) || afterNth s: [] p: 1 w: max(x1 + 62, x2 + 61) || #axxu212 s: [] p: 0 w: x2 || #axxu161 s: [1] p: 0 w: x1 + 1 || nil s: [] p: 9 w: 4 || #axxsnd s: [] p: 0 w: 0 || isLNat s: [] p: 12 w: x1 + 27 || #TIlDePAIR s: [] p: 0 w: x2 + 1 || #axxu21 s: [2,3,1] p: 0 w: x1 + x2 + x3 || axxu41 s: [] p: 14 w: max(x2 + 61) || #axxu142 s: [] p: 0 w: 0 || #axxu202 s: [2] p: 12 w: max(x2) || axxafterNth s: [] p: 1 w: max(x1 + 62, x2 + 61) || mark s: 1 || u12 s: [1] p: 2 w: max(x1 + 33, x2 + 40, x3 + 41) || #axxu152 s: [] p: 0 w: 0 || u203 s: [] p: 9 w: max(x2, x3 + 21, x4 + 12) || #axxu22 s: [] p: 0 w: x2 || axxu71 s: [] p: 12 w: x1 + 13 || u101 s: [] p: 7 w: x2 + 39 || #axxu81 s: [] p: 0 w: 1 || axxsel s: [1] p: 13 w: x1 + x2 + 95 || u201 s: [1,4] p: 11 w: max(x1, x2, x3 + 24, x4 + 12) || u21 s: [] p: 6 w: max(x1 + 5, x2 + 5, x3 + 5) || axxu52 s: [] p: 14 w: 23 || #axxu52 s: [] p: 0 w: 0 || axxu111 s: [] p: 12 w: 23 || axxfst s: [] p: 7 w: x1 + 24 || axxu61 s: [] p: 12 w: 23 || axxu171 s: [] p: 14 w: max(x1 + 94, x2 + 93, x3 + 91) || u161 s: [] p: 13 w: max(x1 + 14, x2 + 14) || #axxu31 s: [1,3] p: 0 w: x1 + x3 + 1 || u204 s: [] p: 5 w: max(x1, x2 + 21) || #axxsel s: [1] p: 0 w: x1 + 1 || #axxu42 s: [] p: 0 w: 0 || axxu51 s: [] p: 13 w: max(x2 + 24) || u171 s: [] p: 14 w: max(x1 + 94, x2 + 93, x3 + 91) || axxu221 s: [] p: 13 w: max(x2 + 38, x3 + 37) || head s: [1] p: 12 w: x1 + 28 || cons s: [1] p: 12 w: max(x1 + 13, x2) || u142 s: [1] p: 3 w: x1 || axxu222 s: [] p: 9 w: max(x2 + 38, x3 + 37) || snd s: [1] p: 3 w: x1 + 28 || #axxu41 s: [] p: 0 w: 0 || u22 s: [] p: 0 w: max(x2 + 4) || axxu12 s: [1] p: 2 w: max(x1 + 33, x2 + 40, x3 + 41) || axxtail s: [1] p: 14 w: x1 + 28 || u42 s: [] p: 14 w: x1 + 1 || tt s: [] p: 14 w: 22 || #axxu191 s: [] p: 0 w: x1 || axxu42 s: [] p: 14 w: x1 + 1 || #axxu131 s: [] p: 0 w: x2 || u152 s: [] p: 12 w: 23 || axxu161 s: [] p: 13 w: max(x1 + 14, x2 + 14) || axxu202 s: [4] p: 10 w: max(x2, x3 + 23, x4 + 12) || u71 s: [] p: 12 w: x1 + 13 || axxtake s: [] p: 13 w: x1 + x2 + 39 || #axxu61 s: [] p: 0 w: 1 || #axxfst s: [] p: 0 w: 0 || #axxu171 s: [2,1,3] p: 0 w: x1 + x2 + x3 || axxu101 s: [] p: 7 w: x2 + 39 || #axxu71 s: [] p: 0 w: 1 || #axxisNatural s: [] p: 0 w: 0 || axxu212 s: [] p: 8 w: max(x2 + 1) || u31 s: [] p: 12 w: max(x2 + 12, x3 + 28) || u141 s: [] p: 4 w: max(x2 + 28) || axxu21 s: [] p: 6 w: max(x1 + 5, x2 + 5, x3 + 5) || #axxu182 s: [] p: 0 w: x2 + 1 || #axxu203 s: [2] p: 12 w: max(x2) || #axxtake s: [2] p: 0 w: x2 || #axxhead s: [] p: 0 w: 1 || axxhead s: [1] p: 12 w: x1 + 28 || USABLE RULES: { 1..168 } || Removed DPs: #161 || 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) => axxu102(axxisLNat(X)) axxu102(tt) => tt axxu11(tt, X, Y) => axxu12(axxisLNat(Y), X, Y) axxu111(tt) => tt axxu12(tt, X, Y) => axxsnd(axxsplitAt(mark(X), mark(Y))) axxu121(tt) => tt axxu131(tt, X) => axxu132(axxisLNat(X)) axxu132(tt) => tt axxu141(tt, X) => axxu142(axxisLNat(X)) axxu142(tt) => tt axxu151(tt, X) => axxu152(axxisLNat(X)) axxu152(tt) => tt axxu161(tt, X) => cons(mark(X), natsFrom(s(X))) axxu171(tt, X, Y) => axxu172(axxisLNat(Y), X, Y) axxu172(tt, X, Y) => axxhead(axxafterNth(mark(X), mark(Y))) axxu181(tt, X) => axxu182(axxisLNat(X), X) axxu182(tt, X) => mark(X) axxu191(tt, X) => pair(nil, mark(X)) axxu201(tt, X, Y, Z) => axxu202(axxisNatural(Y), X, Y, Z) axxu202(tt, X, Y, Z) => axxu203(axxisLNat(Z), X, Y, Z) axxu203(tt, X, Y, Z) => axxu204(axxsplitAt(mark(X), mark(Z)), Y) axxu204(pair(X, Y), Z) => pair(cons(mark(Z), X), mark(Y)) axxu21(tt, X, Y) => axxu22(axxisLNat(Y), X) axxu211(tt, X) => axxu212(axxisLNat(X), X) axxu212(tt, X) => mark(X) axxu22(tt, X) => mark(X) axxu221(tt, X, Y) => axxu222(axxisLNat(Y), X, Y) axxu222(tt, X, Y) => axxfst(axxsplitAt(mark(X), mark(Y))) axxu31(tt, X, Y) => axxu32(axxisLNat(Y), X) axxu32(tt, X) => mark(X) axxu41(tt, X) => axxu42(axxisLNat(X)) axxu42(tt) => tt axxu51(tt, X) => axxu52(axxisLNat(X)) axxu52(tt) => tt axxu61(tt) => tt axxu71(tt) => tt axxu81(tt) => tt axxu91(tt) => tt axxafterNth(X, Y) => axxu11(axxisNatural(X), X, Y) axxfst(pair(X, Y)) => axxu21(axxisLNat(X), X, Y) axxhead(cons(X, Y)) => axxu31(axxisNatural(X), X, Y) axxisLNat(nil) => tt axxisLNat(afterNth(X, Y)) => axxu41(axxisNatural(X), Y) axxisLNat(cons(X, Y)) => axxu51(axxisNatural(X), Y) axxisLNat(fst(X)) => axxu61(axxisPLNat(X)) axxisLNat(natsFrom(X)) => axxu71(axxisNatural(X)) axxisLNat(snd(X)) => axxu81(axxisPLNat(X)) axxisLNat(tail(X)) => axxu91(axxisLNat(X)) axxisLNat(take(X, Y)) => axxu101(axxisNatural(X), Y) axxisNatural(0) => tt axxisNatural(head(X)) => axxu111(axxisLNat(X)) axxisNatural(s(X)) => axxu121(axxisNatural(X)) axxisNatural(sel(X, Y)) => axxu131(axxisNatural(X), Y) axxisPLNat(pair(X, Y)) => axxu141(axxisLNat(X), Y) axxisPLNat(splitAt(X, Y)) => axxu151(axxisNatural(X), Y) axxnatsFrom(X) => axxu161(axxisNatural(X), X) axxsel(X, Y) => axxu171(axxisNatural(X), X, Y) axxsnd(pair(X, Y)) => axxu181(axxisLNat(X), Y) axxsplitAt(0, X) => axxu191(axxisLNat(X), X) axxsplitAt(s(X), cons(Y, Z)) => axxu201(axxisNatural(X), X, Y, Z) axxtail(cons(X, Y)) => axxu211(axxisNatural(X), Y) axxtake(X, Y) => axxu221(axxisNatural(X), X, Y) mark(u101(X, Y)) => axxu101(mark(X), Y) mark(u102(X)) => axxu102(mark(X)) mark(isLNat(X)) => axxisLNat(X) mark(u11(X, Y, Z)) => axxu11(mark(X), Y, Z) mark(u12(X, Y, Z)) => axxu12(mark(X), Y, Z) mark(u111(X)) => axxu111(mark(X)) mark(snd(X)) => axxsnd(mark(X)) mark(splitAt(X, Y)) => axxsplitAt(mark(X), mark(Y)) mark(u121(X)) => axxu121(mark(X)) mark(u131(X, Y)) => axxu131(mark(X), Y) mark(u132(X)) => axxu132(mark(X)) mark(u141(X, Y)) => axxu141(mark(X), Y) mark(u142(X)) => axxu142(mark(X)) mark(u151(X, Y)) => axxu151(mark(X), Y) mark(u152(X)) => axxu152(mark(X)) mark(u161(X, Y)) => axxu161(mark(X), Y) mark(natsFrom(X)) => axxnatsFrom(mark(X)) mark(u171(X, Y, Z)) => axxu171(mark(X), Y, Z) mark(u172(X, Y, Z)) => axxu172(mark(X), Y, Z) mark(head(X)) => axxhead(mark(X)) mark(afterNth(X, Y)) => axxafterNth(mark(X), mark(Y)) mark(u181(X, Y)) => axxu181(mark(X), Y) mark(u182(X, Y)) => axxu182(mark(X), Y) mark(u191(X, Y)) => axxu191(mark(X), Y) mark(u201(X, Y, Z, U)) => axxu201(mark(X), Y, Z, U) mark(u202(X, Y, Z, U)) => axxu202(mark(X), Y, Z, U) mark(isNatural(X)) => axxisNatural(X) mark(u203(X, Y, Z, U)) => axxu203(mark(X), Y, Z, U) mark(u204(X, Y)) => axxu204(mark(X), Y) mark(u21(X, Y, Z)) => axxu21(mark(X), Y, Z) mark(u22(X, Y)) => axxu22(mark(X), Y) mark(u211(X, Y)) => axxu211(mark(X), Y) mark(u212(X, Y)) => axxu212(mark(X), Y) mark(u221(X, Y, Z)) => axxu221(mark(X), Y, Z) mark(u222(X, Y, Z)) => axxu222(mark(X), Y, Z) mark(fst(X)) => axxfst(mark(X)) mark(u31(X, Y, Z)) => axxu31(mark(X), Y, Z) mark(u32(X, Y)) => axxu32(mark(X), Y) mark(u41(X, Y)) => axxu41(mark(X), Y) mark(u42(X)) => axxu42(mark(X)) mark(u51(X, Y)) => axxu51(mark(X), Y) mark(u52(X)) => axxu52(mark(X)) mark(u61(X)) => axxu61(mark(X)) mark(u71(X)) => axxu71(mark(X)) mark(u81(X)) => axxu81(mark(X)) mark(u91(X)) => axxu91(mark(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) => u101(X, Y) axxu102(X) => u102(X) axxisLNat(X) => isLNat(X) axxu11(X, Y, Z) => u11(X, Y, Z) axxu12(X, Y, Z) => u12(X, Y, Z) axxu111(X) => u111(X) axxsnd(X) => snd(X) axxsplitAt(X, Y) => splitAt(X, Y) axxu121(X) => u121(X) axxu131(X, Y) => u131(X, Y) axxu132(X) => u132(X) axxu141(X, Y) => u141(X, Y) axxu142(X) => u142(X) axxu151(X, Y) => u151(X, Y) axxu152(X) => u152(X) axxu161(X, Y) => u161(X, Y) axxnatsFrom(X) => natsFrom(X) axxu171(X, Y, Z) => u171(X, Y, Z) axxu172(X, Y, Z) => u172(X, Y, Z) axxhead(X) => head(X) axxafterNth(X, Y) => afterNth(X, Y) axxu181(X, Y) => u181(X, Y) axxu182(X, Y) => u182(X, Y) axxu191(X, Y) => u191(X, Y) axxu201(X, Y, Z, U) => u201(X, Y, Z, U) axxu202(X, Y, Z, U) => u202(X, Y, Z, U) axxisNatural(X) => isNatural(X) axxu203(X, Y, Z, U) => u203(X, Y, Z, U) axxu204(X, Y) => u204(X, Y) axxu21(X, Y, Z) => u21(X, Y, Z) axxu22(X, Y) => u22(X, Y) axxu211(X, Y) => u211(X, Y) axxu212(X, Y) => u212(X, Y) axxu221(X, Y, Z) => u221(X, Y, Z) axxu222(X, Y, Z) => u222(X, Y, Z) axxfst(X) => fst(X) axxu31(X, Y, Z) => u31(X, Y, Z) axxu32(X, Y) => u32(X, Y) axxu41(X, Y) => u41(X, Y) axxu42(X) => u42(X) axxu51(X, Y) => u51(X, Y) axxu52(X) => u52(X) axxu61(X) => u61(X) axxu71(X) => u71(X) axxu81(X) => u81(X) axxu91(X) => u91(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.