Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nosorts_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,N,X,XS)	→	a__U12(a__splitAt(mark(N),mark(XS)),X)	(1)
a__U12(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(2)
a__afterNth(N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(3)
a__and(tt,X)	→	mark(X)	(4)
a__fst(pair(X,Y))	→	mark(X)	(5)
a__head(cons(N,XS))	→	mark(N)	(6)
a__natsFrom(N)	→	cons(mark(N),natsFrom(s(N)))	(7)
a__sel(N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(8)
a__snd(pair(X,Y))	→	mark(Y)	(9)
a__splitAt(0,XS)	→	pair(nil,mark(XS))	(10)
a__splitAt(s(N),cons(X,XS))	→	a__U11(tt,N,X,XS)	(11)
a__tail(cons(N,XS))	→	mark(XS)	(12)
a__take(N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(13)
mark(U11(X1,X2,X3,X4))	→	a__U11(mark(X1),X2,X3,X4)	(14)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(15)
mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(16)
mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(17)
mark(snd(X))	→	a__snd(mark(X))	(18)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(19)
mark(fst(X))	→	a__fst(mark(X))	(20)
mark(head(X))	→	a__head(mark(X))	(21)
mark(natsFrom(X))	→	a__natsFrom(mark(X))	(22)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(23)
mark(tail(X))	→	a__tail(mark(X))	(24)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(25)
mark(tt)	→	tt	(26)
mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(27)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(28)
mark(s(X))	→	s(mark(X))	(29)
mark(0)	→	0	(30)
mark(nil)	→	nil	(31)
a__U11(X1,X2,X3,X4)	→	U11(X1,X2,X3,X4)	(32)
a__U12(X1,X2)	→	U12(X1,X2)	(33)
a__splitAt(X1,X2)	→	splitAt(X1,X2)	(34)
a__afterNth(X1,X2)	→	afterNth(X1,X2)	(35)
a__snd(X)	→	snd(X)	(36)
a__and(X1,X2)	→	and(X1,X2)	(37)
a__fst(X)	→	fst(X)	(38)
a__head(X)	→	head(X)	(39)
a__natsFrom(X)	→	natsFrom(X)	(40)
a__sel(X1,X2)	→	sel(X1,X2)	(41)
a__tail(X)	→	tail(X)	(42)
a__take(X1,X2)	→	take(X1,X2)	(43)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a__U12^#(pair(YS,ZS),X)	→	mark^#(ZS)	(44)
a__afterNth^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(45)
mark^#(natsFrom(X))	→	mark^#(X)	(46)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(47)
a__U11^#(tt,N,X,XS)	→	a__U12^#(a__splitAt(mark(N),mark(XS)),X)	(48)
a__afterNth^#(N,XS)	→	a__snd^#(a__splitAt(mark(N),mark(XS)))	(49)
mark^#(splitAt(X1,X2))	→	mark^#(X2)	(50)
mark^#(head(X))	→	a__head^#(mark(X))	(51)
a__U11^#(tt,N,X,XS)	→	a__splitAt^#(mark(N),mark(XS))	(52)
a__sel^#(N,XS)	→	mark^#(XS)	(53)
a__U11^#(tt,N,X,XS)	→	mark^#(N)	(54)
mark^#(snd(X))	→	mark^#(X)	(55)
mark^#(head(X))	→	mark^#(X)	(56)
a__take^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(57)
mark^#(U12(X1,X2))	→	mark^#(X1)	(58)
mark^#(splitAt(X1,X2))	→	mark^#(X1)	(59)
a__sel^#(N,XS)	→	a__afterNth^#(mark(N),mark(XS))	(60)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(61)
a__snd^#(pair(X,Y))	→	mark^#(Y)	(62)
mark^#(tail(X))	→	a__tail^#(mark(X))	(63)
mark^#(snd(X))	→	a__snd^#(mark(X))	(64)
a__natsFrom^#(N)	→	mark^#(N)	(65)
mark^#(fst(X))	→	mark^#(X)	(66)
a__afterNth^#(N,XS)	→	mark^#(XS)	(67)
mark^#(tail(X))	→	mark^#(X)	(68)
mark^#(pair(X1,X2))	→	mark^#(X2)	(69)
a__and^#(tt,X)	→	mark^#(X)	(70)
mark^#(sel(X1,X2))	→	mark^#(X1)	(71)
mark^#(pair(X1,X2))	→	mark^#(X1)	(72)
a__sel^#(N,XS)	→	mark^#(N)	(73)
a__U11^#(tt,N,X,XS)	→	mark^#(XS)	(74)
a__splitAt^#(0,XS)	→	mark^#(XS)	(75)
mark^#(take(X1,X2))	→	mark^#(X1)	(76)
a__take^#(N,XS)	→	mark^#(N)	(77)
mark^#(splitAt(X1,X2))	→	a__splitAt^#(mark(X1),mark(X2))	(78)
a__splitAt^#(s(N),cons(X,XS))	→	a__U11^#(tt,N,X,XS)	(79)
mark^#(afterNth(X1,X2))	→	mark^#(X1)	(80)
a__take^#(N,XS)	→	a__fst^#(a__splitAt(mark(N),mark(XS)))	(81)
a__afterNth^#(N,XS)	→	mark^#(N)	(82)
mark^#(natsFrom(X))	→	a__natsFrom^#(mark(X))	(83)
mark^#(fst(X))	→	a__fst^#(mark(X))	(84)
mark^#(afterNth(X1,X2))	→	mark^#(X2)	(85)
mark^#(cons(X1,X2))	→	mark^#(X1)	(86)
mark^#(U11(X1,X2,X3,X4))	→	a__U11^#(mark(X1),X2,X3,X4)	(87)
mark^#(afterNth(X1,X2))	→	a__afterNth^#(mark(X1),mark(X2))	(88)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(89)
a__fst^#(pair(X,Y))	→	mark^#(X)	(90)
mark^#(and(X1,X2))	→	mark^#(X1)	(91)
mark^#(take(X1,X2))	→	mark^#(X2)	(92)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(93)
mark^#(s(X))	→	mark^#(X)	(94)
a__U12^#(pair(YS,ZS),X)	→	mark^#(X)	(95)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(96)
a__take^#(N,XS)	→	mark^#(XS)	(97)
mark^#(sel(X1,X2))	→	mark^#(X2)	(98)
a__head^#(cons(N,XS))	→	mark^#(N)	(99)
a__sel^#(N,XS)	→	a__head^#(a__afterNth(mark(N),mark(XS)))	(100)
mark^#(U11(X1,X2,X3,X4))	→	mark^#(X1)	(101)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(U11(X1,X2,X3,X4))	→	mark^#(X1)	(101)
a__sel^#(N,XS)	→	a__head^#(a__afterNth(mark(N),mark(XS)))	(100)
a__splitAt^#(0,XS)	→	mark^#(XS)	(75)
a__sel^#(N,XS)	→	mark^#(N)	(73)
a__U11^#(tt,N,X,XS)	→	mark^#(XS)	(74)
a__head^#(cons(N,XS))	→	mark^#(N)	(99)
mark^#(pair(X1,X2))	→	mark^#(X1)	(72)
mark^#(sel(X1,X2))	→	mark^#(X1)	(71)
mark^#(sel(X1,X2))	→	mark^#(X2)	(98)
a__and^#(tt,X)	→	mark^#(X)	(70)
mark^#(pair(X1,X2))	→	mark^#(X2)	(69)
mark^#(tail(X))	→	mark^#(X)	(68)
a__take^#(N,XS)	→	mark^#(XS)	(97)
a__afterNth^#(N,XS)	→	mark^#(XS)	(67)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(96)
a__U12^#(pair(YS,ZS),X)	→	mark^#(X)	(95)
mark^#(fst(X))	→	mark^#(X)	(66)
mark^#(s(X))	→	mark^#(X)	(94)
a__natsFrom^#(N)	→	mark^#(N)	(65)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(93)
mark^#(take(X1,X2))	→	mark^#(X2)	(92)
mark^#(and(X1,X2))	→	mark^#(X1)	(91)
mark^#(snd(X))	→	a__snd^#(mark(X))	(64)
a__fst^#(pair(X,Y))	→	mark^#(X)	(90)
mark^#(tail(X))	→	a__tail^#(mark(X))	(63)
a__snd^#(pair(X,Y))	→	mark^#(Y)	(62)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(61)
a__sel^#(N,XS)	→	a__afterNth^#(mark(N),mark(XS))	(60)
mark^#(afterNth(X1,X2))	→	a__afterNth^#(mark(X1),mark(X2))	(88)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(89)
mark^#(U11(X1,X2,X3,X4))	→	a__U11^#(mark(X1),X2,X3,X4)	(87)
mark^#(splitAt(X1,X2))	→	mark^#(X1)	(59)
mark^#(U12(X1,X2))	→	mark^#(X1)	(58)
a__take^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(57)
mark^#(cons(X1,X2))	→	mark^#(X1)	(86)
mark^#(head(X))	→	mark^#(X)	(56)
mark^#(snd(X))	→	mark^#(X)	(55)
mark^#(afterNth(X1,X2))	→	mark^#(X2)	(85)
a__U11^#(tt,N,X,XS)	→	mark^#(N)	(54)
mark^#(fst(X))	→	a__fst^#(mark(X))	(84)
a__sel^#(N,XS)	→	mark^#(XS)	(53)
mark^#(natsFrom(X))	→	a__natsFrom^#(mark(X))	(83)
a__U11^#(tt,N,X,XS)	→	a__splitAt^#(mark(N),mark(XS))	(52)
a__afterNth^#(N,XS)	→	mark^#(N)	(82)
a__take^#(N,XS)	→	a__fst^#(a__splitAt(mark(N),mark(XS)))	(81)
mark^#(head(X))	→	a__head^#(mark(X))	(51)
mark^#(afterNth(X1,X2))	→	mark^#(X1)	(80)
mark^#(splitAt(X1,X2))	→	mark^#(X2)	(50)
a__afterNth^#(N,XS)	→	a__snd^#(a__splitAt(mark(N),mark(XS)))	(49)
a__splitAt^#(s(N),cons(X,XS))	→	a__U11^#(tt,N,X,XS)	(79)
a__U11^#(tt,N,X,XS)	→	a__U12^#(a__splitAt(mark(N),mark(XS)),X)	(48)
mark^#(splitAt(X1,X2))	→	a__splitAt^#(mark(X1),mark(X2))	(78)
a__take^#(N,XS)	→	mark^#(N)	(77)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(47)
mark^#(natsFrom(X))	→	mark^#(X)	(46)
a__afterNth^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(45)
a__U12^#(pair(YS,ZS),X)	→	mark^#(ZS)	(44)
mark^#(take(X1,X2))	→	mark^#(X1)	(76)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	max(x₁ + 37657, x₂ + 37656, x₃ + 37656, x₄ + 37656, 0)
[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	x₁ + 58481
[a__natsFrom^#(x₁)]	=	x₁ + 87762
[a__snd^#(x₁)]	=	x₁ + 37895
[a__afterNth(x₁, x₂)]	=	max(x₁ + 37657, x₂ + 37659, 0)
[take(x₁, x₂)]	=	max(x₁ + 37658, x₂ + 37657, 0)
[and(x₁, x₂)]	=	max(x₁ + 7631, x₂ + 7630, 0)
[pair(x₁, x₂)]	=	max(x₁ + 20588, x₂ + 20588, 0)
[fst(x₁)]	=	x₁ + 1
[natsFrom(x₁)]	=	x₁ + 29280
[a__snd(x₁)]	=	x₁ + 1
[splitAt(x₁, x₂)]	=	max(x₁ + 37656, x₂ + 37656, 0)
[a__U11^#(x₁,...,x₄)]	=	max(x₁ + 79071, x₂ + 96136, x₃ + 96135, x₄ + 96137, 0)
[a__take^#(x₁, x₂)]	=	max(x₁ + 96138, x₂ + 96138, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 37656, 0)
[a__U12^#(x₁, x₂)]	=	max(x₁ + 37894, x₂ + 96135, 0)
[a__fst(x₁)]	=	x₁ + 1
[a__natsFrom(x₁)]	=	x₁ + 29280
[tail(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	x₁ + 58482
[0]	=	60516
[a__and^#(x₁, x₂)]	=	max(x₁ + 41416, x₂ + 58482, 0)
[sel(x₁, x₂)]	=	max(x₁ + 37658, x₂ + 37659, 0)
[afterNth(x₁, x₂)]	=	max(x₁ + 37657, x₂ + 37659, 0)
[nil]	=	12280
[a__splitAt(x₁, x₂)]	=	max(x₁ + 37656, x₂ + 37656, 0)
[a__sel^#(x₁, x₂)]	=	max(x₁ + 96139, x₂ + 96141, 0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁,...,x₄)]	=	max(x₁ + 37657, x₂ + 37656, x₃ + 37656, x₄ + 37656, 0)
[a__sel(x₁, x₂)]	=	max(x₁ + 37658, x₂ + 37659, 0)
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 37656, 0)
[head(x₁)]	=	x₁ + 0
[a__afterNth^#(x₁, x₂)]	=	max(x₁ + 96138, x₂ + 96140, 0)
[a__splitAt^#(x₁, x₂)]	=	max(x₁ + 96136, x₂ + 96137, 0)
[cons(x₁, x₂)]	=	max(x₁ + 17068, x₂ + 0, 0)
[snd(x₁)]	=	x₁ + 1
[a__take(x₁, x₂)]	=	max(x₁ + 37658, x₂ + 37657, 0)
[tt]	=	17067
[a__fst^#(x₁)]	=	x₁ + 37895
[a__and(x₁, x₂)]	=	max(x₁ + 7631, x₂ + 7630, 0)
[a__tail(x₁)]	=	x₁ + 0
[a__tail^#(x₁)]	=	x₁ + 58482
[a__head(x₁)]	=	x₁ + 0

together with the usable rules

mark(snd(X))	→	a__snd(mark(X))	(18)
a__and(tt,X)	→	mark(X)	(4)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(15)
a__sel(N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(8)
a__U11(tt,N,X,XS)	→	a__U12(a__splitAt(mark(N),mark(XS)),X)	(1)
a__afterNth(N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(3)
mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(16)
mark(head(X))	→	a__head(mark(X))	(21)
a__snd(X)	→	snd(X)	(36)
mark(tt)	→	tt	(26)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(19)
a__U11(X1,X2,X3,X4)	→	U11(X1,X2,X3,X4)	(32)
mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(17)
mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(27)
a__splitAt(X1,X2)	→	splitAt(X1,X2)	(34)
mark(natsFrom(X))	→	a__natsFrom(mark(X))	(22)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(28)
a__fst(pair(X,Y))	→	mark(X)	(5)
a__U12(X1,X2)	→	U12(X1,X2)	(33)
a__splitAt(0,XS)	→	pair(nil,mark(XS))	(10)
a__head(X)	→	head(X)	(39)
a__natsFrom(N)	→	cons(mark(N),natsFrom(s(N)))	(7)
mark(fst(X))	→	a__fst(mark(X))	(20)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(25)
mark(0)	→	0	(30)
mark(U11(X1,X2,X3,X4))	→	a__U11(mark(X1),X2,X3,X4)	(14)
mark(nil)	→	nil	(31)
a__tail(cons(N,XS))	→	mark(XS)	(12)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(23)
mark(tail(X))	→	a__tail(mark(X))	(24)
a__splitAt(s(N),cons(X,XS))	→	a__U11(tt,N,X,XS)	(11)
a__snd(pair(X,Y))	→	mark(Y)	(9)
a__take(N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(13)
a__natsFrom(X)	→	natsFrom(X)	(40)
a__head(cons(N,XS))	→	mark(N)	(6)
a__fst(X)	→	fst(X)	(38)
a__and(X1,X2)	→	and(X1,X2)	(37)
a__sel(X1,X2)	→	sel(X1,X2)	(41)
a__tail(X)	→	tail(X)	(42)
a__afterNth(X1,X2)	→	afterNth(X1,X2)	(35)
mark(s(X))	→	s(mark(X))	(29)
a__take(X1,X2)	→	take(X1,X2)	(43)
a__U12(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

mark^#(U11(X1,X2,X3,X4))	→	mark^#(X1)	(101)
a__sel^#(N,XS)	→	a__head^#(a__afterNth(mark(N),mark(XS)))	(100)
a__splitAt^#(0,XS)	→	mark^#(XS)	(75)
a__sel^#(N,XS)	→	mark^#(N)	(73)
a__U11^#(tt,N,X,XS)	→	mark^#(XS)	(74)
a__head^#(cons(N,XS))	→	mark^#(N)	(99)
mark^#(pair(X1,X2))	→	mark^#(X1)	(72)
mark^#(sel(X1,X2))	→	mark^#(X1)	(71)
mark^#(sel(X1,X2))	→	mark^#(X2)	(98)
mark^#(pair(X1,X2))	→	mark^#(X2)	(69)
a__take^#(N,XS)	→	mark^#(XS)	(97)
a__afterNth^#(N,XS)	→	mark^#(XS)	(67)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(96)
a__U12^#(pair(YS,ZS),X)	→	mark^#(X)	(95)
mark^#(fst(X))	→	mark^#(X)	(66)
a__natsFrom^#(N)	→	mark^#(N)	(65)
mark^#(take(X1,X2))	→	mark^#(X2)	(92)
mark^#(and(X1,X2))	→	mark^#(X1)	(91)
mark^#(snd(X))	→	a__snd^#(mark(X))	(64)
a__fst^#(pair(X,Y))	→	mark^#(X)	(90)
a__snd^#(pair(X,Y))	→	mark^#(Y)	(62)
a__sel^#(N,XS)	→	a__afterNth^#(mark(N),mark(XS))	(60)
mark^#(afterNth(X1,X2))	→	a__afterNth^#(mark(X1),mark(X2))	(88)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(89)
mark^#(U11(X1,X2,X3,X4))	→	a__U11^#(mark(X1),X2,X3,X4)	(87)
mark^#(splitAt(X1,X2))	→	mark^#(X1)	(59)
a__take^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(57)
mark^#(cons(X1,X2))	→	mark^#(X1)	(86)
mark^#(snd(X))	→	mark^#(X)	(55)
mark^#(afterNth(X1,X2))	→	mark^#(X2)	(85)
a__U11^#(tt,N,X,XS)	→	mark^#(N)	(54)
mark^#(fst(X))	→	a__fst^#(mark(X))	(84)
a__sel^#(N,XS)	→	mark^#(XS)	(53)
a__afterNth^#(N,XS)	→	mark^#(N)	(82)
a__take^#(N,XS)	→	a__fst^#(a__splitAt(mark(N),mark(XS)))	(81)
mark^#(head(X))	→	a__head^#(mark(X))	(51)
mark^#(afterNth(X1,X2))	→	mark^#(X1)	(80)
mark^#(splitAt(X1,X2))	→	mark^#(X2)	(50)
a__afterNth^#(N,XS)	→	a__snd^#(a__splitAt(mark(N),mark(XS)))	(49)
mark^#(splitAt(X1,X2))	→	a__splitAt^#(mark(X1),mark(X2))	(78)
a__take^#(N,XS)	→	mark^#(N)	(77)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(47)
mark^#(natsFrom(X))	→	mark^#(X)	(46)
a__afterNth^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(45)
mark^#(take(X1,X2))	→	mark^#(X1)	(76)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__U11^#(tt,N,X,XS)	→	a__splitAt^#(mark(N),mark(XS))	(52)
a__splitAt^#(s(N),cons(X,XS))	→	a__U11^#(tt,N,X,XS)	(79)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__natsFrom^#)	=	1
π(and)	=	2
π(fst)	=	1
π(a__snd)	=	1
π(a__fst)	=	1
π(mark^#)	=	1
π(mark)	=	1
π(snd)	=	1
π(a__and)	=	2
π(a__tail^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(U11)	=	6	status(U11)	=	[]	list-extension(U11)	=	Lex
prec(s)	=	6	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__head^#)	=	0	status(a__head^#)	=	[]	list-extension(a__head^#)	=	Lex
prec(a__snd^#)	=	0	status(a__snd^#)	=	[]	list-extension(a__snd^#)	=	Lex
prec(a__afterNth)	=	4	status(a__afterNth)	=	[]	list-extension(a__afterNth)	=	Lex
prec(take)	=	4	status(take)	=	[1]	list-extension(take)	=	Lex
prec(pair)	=	0	status(pair)	=	[]	list-extension(pair)	=	Lex
prec(natsFrom)	=	5	status(natsFrom)	=	[]	list-extension(natsFrom)	=	Lex
prec(splitAt)	=	6	status(splitAt)	=	[2]	list-extension(splitAt)	=	Lex
prec(a__U11^#)	=	3	status(a__U11^#)	=	[2]	list-extension(a__U11^#)	=	Lex
prec(a__take^#)	=	0	status(a__take^#)	=	[1, 2]	list-extension(a__take^#)	=	Lex
prec(U12)	=	1	status(U12)	=	[]	list-extension(U12)	=	Lex
prec(a__U12^#)	=	0	status(a__U12^#)	=	[1]	list-extension(a__U12^#)	=	Lex
prec(a__natsFrom)	=	5	status(a__natsFrom)	=	[]	list-extension(a__natsFrom)	=	Lex
prec(tail)	=	4	status(tail)	=	[]	list-extension(tail)	=	Lex
prec(0)	=	5	status(0)	=	[]	list-extension(0)	=	Lex
prec(a__and^#)	=	0	status(a__and^#)	=	[]	list-extension(a__and^#)	=	Lex
prec(sel)	=	3	status(sel)	=	[2]	list-extension(sel)	=	Lex
prec(afterNth)	=	4	status(afterNth)	=	[]	list-extension(afterNth)	=	Lex
prec(nil)	=	6	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(a__splitAt)	=	6	status(a__splitAt)	=	[2]	list-extension(a__splitAt)	=	Lex
prec(a__sel^#)	=	0	status(a__sel^#)	=	[]	list-extension(a__sel^#)	=	Lex
prec(a__U11)	=	6	status(a__U11)	=	[]	list-extension(a__U11)	=	Lex
prec(a__sel)	=	3	status(a__sel)	=	[2]	list-extension(a__sel)	=	Lex
prec(a__U12)	=	1	status(a__U12)	=	[]	list-extension(a__U12)	=	Lex
prec(head)	=	2	status(head)	=	[]	list-extension(head)	=	Lex
prec(a__afterNth^#)	=	0	status(a__afterNth^#)	=	[2]	list-extension(a__afterNth^#)	=	Lex
prec(a__splitAt^#)	=	3	status(a__splitAt^#)	=	[1]	list-extension(a__splitAt^#)	=	Lex
prec(cons)	=	2	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(a__take)	=	4	status(a__take)	=	[1]	list-extension(a__take)	=	Lex
prec(tt)	=	6	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(a__fst^#)	=	0	status(a__fst^#)	=	[]	list-extension(a__fst^#)	=	Lex
prec(a__tail)	=	4	status(a__tail)	=	[]	list-extension(a__tail)	=	Lex
prec(a__head)	=	2	status(a__head)	=	[]	list-extension(a__head)	=	Lex

and the following Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	max(x₁ + 24567, x₃ + 24568, x₄ + 24570, 0)
[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	1
[a__snd^#(x₁)]	=	1
[a__afterNth(x₁, x₂)]	=	x₂ + 24571
[take(x₁, x₂)]	=	x₁ + x₂ + 24571
[pair(x₁, x₂)]	=	max(x₁ + 12284, x₂ + 24569, 0)
[natsFrom(x₁)]	=	x₁ + 12284
[splitAt(x₁, x₂)]	=	max(x₂ + 24570, 0)
[a__U11^#(x₁,...,x₄)]	=	max(x₁ + 0, x₂ + 12282, x₃ + 12285, x₄ + 12284, 0)
[a__take^#(x₁, x₂)]	=	x₁ + x₂ + 1
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 24568, 0)
[a__U12^#(x₁, x₂)]	=	max(x₁ + 1, 0)
[a__natsFrom(x₁)]	=	x₁ + 12284
[tail(x₁)]	=	x₁ + 1
[0]	=	0
[a__and^#(x₁, x₂)]	=	x₁ + 1
[sel(x₁, x₂)]	=	x₂ + 38080
[afterNth(x₁, x₂)]	=	x₂ + 24571
[nil]	=	0
[a__splitAt(x₁, x₂)]	=	max(x₂ + 24570, 0)
[a__sel^#(x₁, x₂)]	=	x₂ + 1
[a__U11(x₁,...,x₄)]	=	max(x₁ + 24567, x₃ + 24568, x₄ + 24570, 0)
[a__sel(x₁, x₂)]	=	x₂ + 38080
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 24568, 0)
[head(x₁)]	=	x₁ + 13508
[a__afterNth^#(x₁, x₂)]	=	x₂ + 1
[a__splitAt^#(x₁, x₂)]	=	max(x₁ + 12282, x₂ + 12284, 0)
[cons(x₁, x₂)]	=	max(x₁ + 12283, x₂ + 0, 0)
[a__take(x₁, x₂)]	=	x₁ + x₂ + 24571
[tt]	=	12283
[a__fst^#(x₁)]	=	1
[a__tail(x₁)]	=	x₁ + 1
[a__head(x₁)]	=	x₁ + 13508

together with the usable rules

mark(snd(X))	→	a__snd(mark(X))	(18)
a__and(tt,X)	→	mark(X)	(4)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(15)
a__sel(N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(8)
a__U11(tt,N,X,XS)	→	a__U12(a__splitAt(mark(N),mark(XS)),X)	(1)
a__afterNth(N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(3)
mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(16)
mark(head(X))	→	a__head(mark(X))	(21)
a__snd(X)	→	snd(X)	(36)
mark(tt)	→	tt	(26)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(19)
a__U11(X1,X2,X3,X4)	→	U11(X1,X2,X3,X4)	(32)
mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(17)
mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(27)
a__splitAt(X1,X2)	→	splitAt(X1,X2)	(34)
mark(natsFrom(X))	→	a__natsFrom(mark(X))	(22)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(28)
a__fst(pair(X,Y))	→	mark(X)	(5)
a__U12(X1,X2)	→	U12(X1,X2)	(33)
a__splitAt(0,XS)	→	pair(nil,mark(XS))	(10)
a__head(X)	→	head(X)	(39)
a__natsFrom(N)	→	cons(mark(N),natsFrom(s(N)))	(7)
mark(fst(X))	→	a__fst(mark(X))	(20)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(25)
mark(0)	→	0	(30)
mark(U11(X1,X2,X3,X4))	→	a__U11(mark(X1),X2,X3,X4)	(14)
mark(nil)	→	nil	(31)
a__tail(cons(N,XS))	→	mark(XS)	(12)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(23)
mark(tail(X))	→	a__tail(mark(X))	(24)
a__splitAt(s(N),cons(X,XS))	→	a__U11(tt,N,X,XS)	(11)
a__snd(pair(X,Y))	→	mark(Y)	(9)
a__take(N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(13)
a__natsFrom(X)	→	natsFrom(X)	(40)
a__head(cons(N,XS))	→	mark(N)	(6)
a__fst(X)	→	fst(X)	(38)
a__and(X1,X2)	→	and(X1,X2)	(37)
a__sel(X1,X2)	→	sel(X1,X2)	(41)
a__tail(X)	→	tail(X)	(42)
a__afterNth(X1,X2)	→	afterNth(X1,X2)	(35)
mark(s(X))	→	s(mark(X))	(29)
a__take(X1,X2)	→	take(X1,X2)	(43)
a__U12(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pair

a__splitAt^#(s(N),cons(X,XS))

→

a__U11^#(tt,N,X,XS)

(79)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

mark^#(U12(X1,X2))	→	mark^#(X1)	(58)
mark^#(head(X))	→	mark^#(X)	(56)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(93)
mark^#(tail(X))	→	mark^#(X)	(68)
mark^#(tail(X))	→	a__tail^#(mark(X))	(63)
mark^#(s(X))	→	mark^#(X)	(94)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	max(x₁ + 4, x₃ + 3, x₄ + 2, 0)
[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	58481
[a__natsFrom^#(x₁)]	=	87762
[a__snd^#(x₁)]	=	37895
[a__afterNth(x₁, x₂)]	=	max(x₁ + 3, x₂ + 4, 0)
[take(x₁, x₂)]	=	max(x₁ + 3, x₂ + 4, 0)
[and(x₁, x₂)]	=	max(x₂ + 1, 0)
[pair(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[fst(x₁)]	=	x₁ + 1
[natsFrom(x₁)]	=	x₁ + 9049
[a__snd(x₁)]	=	x₁ + 1
[splitAt(x₁, x₂)]	=	max(x₂ + 2, 0)
[a__U11^#(x₁,...,x₄)]	=	max(0)
[a__take^#(x₁, x₂)]	=	max(0)
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 3, 0)
[a__U12^#(x₁, x₂)]	=	max(0)
[a__fst(x₁)]	=	x₁ + 1
[a__natsFrom(x₁)]	=	x₁ + 9049
[tail(x₁)]	=	x₁ + 2
[mark^#(x₁)]	=	x₁ + 58481
[0]	=	25828
[a__and^#(x₁, x₂)]	=	max(0)
[sel(x₁, x₂)]	=	max(x₁ + 4, x₂ + 5, 0)
[afterNth(x₁, x₂)]	=	max(x₁ + 3, x₂ + 4, 0)
[nil]	=	1
[a__splitAt(x₁, x₂)]	=	max(x₂ + 2, 0)
[a__sel^#(x₁, x₂)]	=	max(0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁,...,x₄)]	=	max(x₁ + 4, x₃ + 3, x₄ + 2, 0)
[a__sel(x₁, x₂)]	=	max(x₁ + 4, x₂ + 5, 0)
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 3, 0)
[head(x₁)]	=	x₁ + 1
[a__afterNth^#(x₁, x₂)]	=	max(0)
[a__splitAt^#(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[snd(x₁)]	=	x₁ + 1
[a__take(x₁, x₂)]	=	max(x₁ + 3, x₂ + 4, 0)
[tt]	=	0
[a__fst^#(x₁)]	=	37895
[a__and(x₁, x₂)]	=	max(x₂ + 1, 0)
[a__tail(x₁)]	=	x₁ + 2
[a__tail^#(x₁)]	=	x₁ + 58482
[a__head(x₁)]	=	x₁ + 1

together with the usable rules

mark(snd(X))	→	a__snd(mark(X))	(18)
a__and(tt,X)	→	mark(X)	(4)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(15)
a__sel(N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(8)
a__U11(tt,N,X,XS)	→	a__U12(a__splitAt(mark(N),mark(XS)),X)	(1)
a__afterNth(N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(3)
mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(16)
mark(head(X))	→	a__head(mark(X))	(21)
a__snd(X)	→	snd(X)	(36)
mark(tt)	→	tt	(26)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(19)
a__U11(X1,X2,X3,X4)	→	U11(X1,X2,X3,X4)	(32)
mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(17)
mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(27)
a__splitAt(X1,X2)	→	splitAt(X1,X2)	(34)
mark(natsFrom(X))	→	a__natsFrom(mark(X))	(22)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(28)
a__fst(pair(X,Y))	→	mark(X)	(5)
a__U12(X1,X2)	→	U12(X1,X2)	(33)
a__splitAt(0,XS)	→	pair(nil,mark(XS))	(10)
a__head(X)	→	head(X)	(39)
a__natsFrom(N)	→	cons(mark(N),natsFrom(s(N)))	(7)
mark(fst(X))	→	a__fst(mark(X))	(20)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(25)
mark(0)	→	0	(30)
mark(U11(X1,X2,X3,X4))	→	a__U11(mark(X1),X2,X3,X4)	(14)
mark(nil)	→	nil	(31)
a__tail(cons(N,XS))	→	mark(XS)	(12)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(23)
mark(tail(X))	→	a__tail(mark(X))	(24)
a__splitAt(s(N),cons(X,XS))	→	a__U11(tt,N,X,XS)	(11)
a__snd(pair(X,Y))	→	mark(Y)	(9)
a__take(N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(13)
a__natsFrom(X)	→	natsFrom(X)	(40)
a__head(cons(N,XS))	→	mark(N)	(6)
a__fst(X)	→	fst(X)	(38)
a__and(X1,X2)	→	and(X1,X2)	(37)
a__sel(X1,X2)	→	sel(X1,X2)	(41)
a__tail(X)	→	tail(X)	(42)
a__afterNth(X1,X2)	→	afterNth(X1,X2)	(35)
mark(s(X))	→	s(mark(X))	(29)
a__take(X1,X2)	→	take(X1,X2)	(43)
a__U12(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

mark^#(head(X))	→	mark^#(X)	(56)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(93)
mark^#(tail(X))	→	mark^#(X)	(68)
mark^#(tail(X))	→	a__tail^#(mark(X))	(63)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(U12(X1,X2))	→	mark^#(X1)	(58)
mark^#(s(X))	→	mark^#(X)	(94)

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + 6
[s(x₁)]	=	x₁ + 1
[a__head^#(x₁)]	=	0
[a__natsFrom^#(x₁)]	=	0
[a__snd^#(x₁)]	=	0
[a__afterNth(x₁, x₂)]	=	x₂ + 1
[take(x₁, x₂)]	=	x₂ + 5
[and(x₁, x₂)]	=	x₁ + x₂ + 5
[pair(x₁, x₂)]	=	x₁ + 1
[fst(x₁)]	=	2
[natsFrom(x₁)]	=	5
[a__snd(x₁)]	=	2
[splitAt(x₁, x₂)]	=	x₁ + 5
[a__U11^#(x₁,...,x₄)]	=	0
[a__take^#(x₁, x₂)]	=	0
[U12(x₁, x₂)]	=	x₁ + x₂ + 3
[a__U12^#(x₁, x₂)]	=	0
[a__fst(x₁)]	=	x₁ + 1
[a__natsFrom(x₁)]	=	4
[tail(x₁)]	=	x₁ + 5
[mark^#(x₁)]	=	x₁ + 1
[0]	=	4
[a__and^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + 2
[afterNth(x₁, x₂)]	=	x₁ + 2
[nil]	=	4
[a__splitAt(x₁, x₂)]	=	4
[a__sel^#(x₁, x₂)]	=	0
[mark(x₁)]	=	3
[a__U11(x₁,...,x₄)]	=	x₄ + 5
[a__sel(x₁, x₂)]	=	x₂ + 1
[a__U12(x₁, x₂)]	=	x₁ + 2
[head(x₁)]	=	5
[a__afterNth^#(x₁, x₂)]	=	0
[a__splitAt^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	5
[snd(x₁)]	=	3
[a__take(x₁, x₂)]	=	4
[tt]	=	4
[a__fst^#(x₁)]	=	0
[a__and(x₁, x₂)]	=	4
[a__tail(x₁)]	=	4
[a__tail^#(x₁)]	=	0
[a__head(x₁)]	=	x₁ + 4

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

mark^#(U12(X1,X2))	→	mark^#(X1)	(58)
mark^#(s(X))	→	mark^#(X)	(94)

could be deleted.

1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.