Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec4_2_DLMMU04_GM)

The rewrite relation of the following TRS is considered.

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

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__u^#(pair(YS,ZS),N,X,XS)	→	mark^#(X)	(37)
mark^#(u(X1,X2,X3,X4))	→	mark^#(X1)	(38)
a__splitAt^#(s(N),cons(X,XS))	→	a__u^#(a__splitAt(mark(N),mark(XS)),N,X,XS)	(39)
mark^#(head(X))	→	mark^#(X)	(40)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(41)
mark^#(u(X1,X2,X3,X4))	→	a__u^#(mark(X1),X2,X3,X4)	(42)
mark^#(take(X1,X2))	→	mark^#(X2)	(43)
mark^#(sel(X1,X2))	→	mark^#(X1)	(44)
mark^#(splitAt(X1,X2))	→	a__splitAt^#(mark(X1),mark(X2))	(45)
mark^#(splitAt(X1,X2))	→	mark^#(X1)	(46)
mark^#(sel(X1,X2))	→	mark^#(X2)	(47)
a__sel^#(N,XS)	→	a__head^#(a__afterNth(mark(N),mark(XS)))	(48)
mark^#(take(X1,X2))	→	mark^#(X1)	(49)
mark^#(tail(X))	→	a__tail^#(mark(X))	(50)
a__afterNth^#(N,XS)	→	mark^#(XS)	(51)
a__sel^#(N,XS)	→	mark^#(XS)	(52)
a__afterNth^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(53)
a__head^#(cons(N,XS))	→	mark^#(N)	(54)
mark^#(afterNth(X1,X2))	→	mark^#(X2)	(55)
a__natsFrom^#(N)	→	mark^#(N)	(56)
a__afterNth^#(N,XS)	→	mark^#(N)	(57)
a__splitAt^#(s(N),cons(X,XS))	→	mark^#(N)	(58)
mark^#(pair(X1,X2))	→	mark^#(X1)	(59)
a__splitAt^#(s(N),cons(X,XS))	→	a__splitAt^#(mark(N),mark(XS))	(60)
mark^#(tail(X))	→	mark^#(X)	(61)
mark^#(splitAt(X1,X2))	→	mark^#(X2)	(62)
a__take^#(N,XS)	→	a__fst^#(a__splitAt(mark(N),mark(XS)))	(63)
mark^#(snd(X))	→	mark^#(X)	(64)
a__sel^#(N,XS)	→	a__afterNth^#(mark(N),mark(XS))	(65)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(66)
a__afterNth^#(N,XS)	→	a__snd^#(a__splitAt(mark(N),mark(XS)))	(67)
mark^#(cons(X1,X2))	→	mark^#(X1)	(68)
mark^#(fst(X))	→	mark^#(X)	(69)
a__snd^#(pair(XS,YS))	→	mark^#(YS)	(70)
a__take^#(N,XS)	→	mark^#(XS)	(71)
mark^#(afterNth(X1,X2))	→	mark^#(X1)	(72)
mark^#(head(X))	→	a__head^#(mark(X))	(73)
a__take^#(N,XS)	→	mark^#(N)	(74)
mark^#(natsFrom(X))	→	a__natsFrom^#(mark(X))	(75)
a__splitAt^#(s(N),cons(X,XS))	→	mark^#(XS)	(76)
mark^#(snd(X))	→	a__snd^#(mark(X))	(77)
a__take^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(78)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(79)
mark^#(afterNth(X1,X2))	→	a__afterNth^#(mark(X1),mark(X2))	(80)
mark^#(s(X))	→	mark^#(X)	(81)
a__u^#(pair(YS,ZS),N,X,XS)	→	mark^#(ZS)	(82)
a__fst^#(pair(XS,YS))	→	mark^#(XS)	(83)
a__sel^#(N,XS)	→	mark^#(N)	(84)
mark^#(pair(X1,X2))	→	mark^#(X2)	(85)
mark^#(fst(X))	→	a__fst^#(mark(X))	(86)
a__splitAt^#(0,XS)	→	mark^#(XS)	(87)
mark^#(natsFrom(X))	→	mark^#(X)	(88)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(natsFrom(X))	→	mark^#(X)	(88)
a__splitAt^#(0,XS)	→	mark^#(XS)	(87)
a__take^#(N,XS)	→	a__fst^#(a__splitAt(mark(N),mark(XS)))	(63)
mark^#(tail(X))	→	mark^#(X)	(61)
mark^#(splitAt(X1,X2))	→	mark^#(X2)	(62)
mark^#(fst(X))	→	a__fst^#(mark(X))	(86)
a__splitAt^#(s(N),cons(X,XS))	→	a__splitAt^#(mark(N),mark(XS))	(60)
mark^#(pair(X1,X2))	→	mark^#(X1)	(59)
mark^#(pair(X1,X2))	→	mark^#(X2)	(85)
a__splitAt^#(s(N),cons(X,XS))	→	mark^#(N)	(58)
a__afterNth^#(N,XS)	→	mark^#(N)	(57)
a__sel^#(N,XS)	→	mark^#(N)	(84)
a__natsFrom^#(N)	→	mark^#(N)	(56)
a__fst^#(pair(XS,YS))	→	mark^#(XS)	(83)
mark^#(afterNth(X1,X2))	→	mark^#(X2)	(55)
a__u^#(pair(YS,ZS),N,X,XS)	→	mark^#(ZS)	(82)
a__head^#(cons(N,XS))	→	mark^#(N)	(54)
mark^#(s(X))	→	mark^#(X)	(81)
mark^#(afterNth(X1,X2))	→	a__afterNth^#(mark(X1),mark(X2))	(80)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(79)
a__take^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(78)
a__afterNth^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(53)
a__sel^#(N,XS)	→	mark^#(XS)	(52)
a__afterNth^#(N,XS)	→	mark^#(XS)	(51)
mark^#(tail(X))	→	a__tail^#(mark(X))	(50)
a__splitAt^#(s(N),cons(X,XS))	→	mark^#(XS)	(76)
mark^#(snd(X))	→	a__snd^#(mark(X))	(77)
mark^#(natsFrom(X))	→	a__natsFrom^#(mark(X))	(75)
mark^#(take(X1,X2))	→	mark^#(X1)	(49)
a__sel^#(N,XS)	→	a__head^#(a__afterNth(mark(N),mark(XS)))	(48)
a__take^#(N,XS)	→	mark^#(N)	(74)
mark^#(sel(X1,X2))	→	mark^#(X2)	(47)
mark^#(head(X))	→	a__head^#(mark(X))	(73)
mark^#(splitAt(X1,X2))	→	mark^#(X1)	(46)
mark^#(afterNth(X1,X2))	→	mark^#(X1)	(72)
a__take^#(N,XS)	→	mark^#(XS)	(71)
mark^#(splitAt(X1,X2))	→	a__splitAt^#(mark(X1),mark(X2))	(45)
a__snd^#(pair(XS,YS))	→	mark^#(YS)	(70)
mark^#(fst(X))	→	mark^#(X)	(69)
mark^#(sel(X1,X2))	→	mark^#(X1)	(44)
mark^#(cons(X1,X2))	→	mark^#(X1)	(68)
mark^#(take(X1,X2))	→	mark^#(X2)	(43)
mark^#(u(X1,X2,X3,X4))	→	a__u^#(mark(X1),X2,X3,X4)	(42)
a__afterNth^#(N,XS)	→	a__snd^#(a__splitAt(mark(N),mark(XS)))	(67)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(41)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(66)
a__sel^#(N,XS)	→	a__afterNth^#(mark(N),mark(XS))	(65)
mark^#(head(X))	→	mark^#(X)	(40)
a__splitAt^#(s(N),cons(X,XS))	→	a__u^#(a__splitAt(mark(N),mark(XS)),N,X,XS)	(39)
mark^#(u(X1,X2,X3,X4))	→	mark^#(X1)	(38)
a__u^#(pair(YS,ZS),N,X,XS)	→	mark^#(X)	(37)
mark^#(snd(X))	→	mark^#(X)	(64)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	x₁ + 74785
[a__natsFrom^#(x₁)]	=	x₁ + 67156
[a__snd^#(x₁)]	=	x₁ + 67154
[a__afterNth(x₁, x₂)]	=	max(x₁ + 60531, x₂ + 60532, 0)
[u(x₁,...,x₄)]	=	max(x₁ + 0, x₂ + 60525, x₃ + 60531, x₄ + 60527, 0)
[take(x₁, x₂)]	=	max(x₁ + 60531, x₂ + 60532, 0)
[pair(x₁, x₂)]	=	max(x₁ + 31118, x₂ + 60525, 0)
[fst(x₁)]	=	x₁ + 1
[natsFrom(x₁)]	=	x₁ + 29407
[a__snd(x₁)]	=	x₁ + 1
[splitAt(x₁, x₂)]	=	max(x₁ + 60530, x₂ + 60528, 0)
[a__take^#(x₁, x₂)]	=	max(x₁ + 127681, x₂ + 127683, 0)
[a__natsFrom(x₁)]	=	x₁ + 29407
[a__fst(x₁)]	=	x₁ + 1
[tail(x₁)]	=	x₁ + 2
[mark^#(x₁)]	=	x₁ + 67155
[0]	=	21084
[a__u(x₁,...,x₄)]	=	max(x₁ + 0, x₂ + 60525, x₃ + 60531, x₄ + 60527, 0)
[sel(x₁, x₂)]	=	max(x₁ + 68163, x₂ + 68164, 0)
[afterNth(x₁, x₂)]	=	max(x₁ + 60531, x₂ + 60532, 0)
[nil]	=	12280
[a__splitAt(x₁, x₂)]	=	max(x₁ + 60530, x₂ + 60528, 0)
[a__sel^#(x₁, x₂)]	=	max(x₁ + 135316, x₂ + 135317, 0)
[mark(x₁)]	=	x₁ + 0
[a__sel(x₁, x₂)]	=	max(x₁ + 68163, x₂ + 68164, 0)
[head(x₁)]	=	x₁ + 7632
[a__afterNth^#(x₁, x₂)]	=	max(x₁ + 127685, x₂ + 127683, 0)
[a__splitAt^#(x₁, x₂)]	=	max(x₁ + 127680, x₂ + 127682, 0)
[cons(x₁, x₂)]	=	max(x₁ + 29407, x₂ + 0, 0)
[snd(x₁)]	=	x₁ + 1
[a__u^#(x₁,...,x₄)]	=	max(x₁ + 36038, x₂ + 67156, x₃ + 127683, x₄ + 127681, 0)
[a__take(x₁, x₂)]	=	max(x₁ + 60531, x₂ + 60532, 0)
[a__fst^#(x₁)]	=	x₁ + 67150
[a__tail(x₁)]	=	x₁ + 2
[a__tail^#(x₁)]	=	x₁ + 67156
[a__head(x₁)]	=	x₁ + 7632

together with the usable rules

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

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

mark^#(natsFrom(X))	→	mark^#(X)	(88)
a__splitAt^#(0,XS)	→	mark^#(XS)	(87)
a__take^#(N,XS)	→	a__fst^#(a__splitAt(mark(N),mark(XS)))	(63)
mark^#(tail(X))	→	mark^#(X)	(61)
mark^#(splitAt(X1,X2))	→	mark^#(X2)	(62)
mark^#(fst(X))	→	a__fst^#(mark(X))	(86)
mark^#(pair(X1,X2))	→	mark^#(X1)	(59)
mark^#(pair(X1,X2))	→	mark^#(X2)	(85)
a__splitAt^#(s(N),cons(X,XS))	→	mark^#(N)	(58)
a__afterNth^#(N,XS)	→	mark^#(N)	(57)
a__sel^#(N,XS)	→	mark^#(N)	(84)
a__natsFrom^#(N)	→	mark^#(N)	(56)
a__fst^#(pair(XS,YS))	→	mark^#(XS)	(83)
mark^#(afterNth(X1,X2))	→	mark^#(X2)	(55)
a__u^#(pair(YS,ZS),N,X,XS)	→	mark^#(ZS)	(82)
a__head^#(cons(N,XS))	→	mark^#(N)	(54)
mark^#(afterNth(X1,X2))	→	a__afterNth^#(mark(X1),mark(X2))	(80)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(79)
a__take^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(78)
a__afterNth^#(N,XS)	→	a__splitAt^#(mark(N),mark(XS))	(53)
a__sel^#(N,XS)	→	mark^#(XS)	(52)
a__afterNth^#(N,XS)	→	mark^#(XS)	(51)
mark^#(tail(X))	→	a__tail^#(mark(X))	(50)
a__splitAt^#(s(N),cons(X,XS))	→	mark^#(XS)	(76)
mark^#(snd(X))	→	a__snd^#(mark(X))	(77)
mark^#(natsFrom(X))	→	a__natsFrom^#(mark(X))	(75)
mark^#(take(X1,X2))	→	mark^#(X1)	(49)
a__take^#(N,XS)	→	mark^#(N)	(74)
mark^#(sel(X1,X2))	→	mark^#(X2)	(47)
mark^#(head(X))	→	a__head^#(mark(X))	(73)
mark^#(splitAt(X1,X2))	→	mark^#(X1)	(46)
mark^#(afterNth(X1,X2))	→	mark^#(X1)	(72)
a__take^#(N,XS)	→	mark^#(XS)	(71)
mark^#(splitAt(X1,X2))	→	a__splitAt^#(mark(X1),mark(X2))	(45)
a__snd^#(pair(XS,YS))	→	mark^#(YS)	(70)
mark^#(fst(X))	→	mark^#(X)	(69)
mark^#(sel(X1,X2))	→	mark^#(X1)	(44)
mark^#(cons(X1,X2))	→	mark^#(X1)	(68)
mark^#(take(X1,X2))	→	mark^#(X2)	(43)
mark^#(u(X1,X2,X3,X4))	→	a__u^#(mark(X1),X2,X3,X4)	(42)
a__afterNth^#(N,XS)	→	a__snd^#(a__splitAt(mark(N),mark(XS)))	(67)
a__tail^#(cons(N,XS))	→	mark^#(XS)	(41)
mark^#(take(X1,X2))	→	a__take^#(mark(X1),mark(X2))	(66)
a__sel^#(N,XS)	→	a__afterNth^#(mark(N),mark(XS))	(65)
mark^#(head(X))	→	mark^#(X)	(40)
a__splitAt^#(s(N),cons(X,XS))	→	a__u^#(a__splitAt(mark(N),mark(XS)),N,X,XS)	(39)
a__u^#(pair(YS,ZS),N,X,XS)	→	mark^#(X)	(37)
mark^#(snd(X))	→	mark^#(X)	(64)

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__splitAt^#(s(N),cons(X,XS))

→

a__splitAt^#(mark(N),mark(XS))

(60)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__natsFrom^#)	=	1
π(mark)	=	1

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

prec(s)	=	4	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)	=	6	status(a__afterNth)	=	[]	list-extension(a__afterNth)	=	Lex
prec(u)	=	3	status(u)	=	[4]	list-extension(u)	=	Lex
prec(take)	=	6	status(take)	=	[]	list-extension(take)	=	Lex
prec(pair)	=	2	status(pair)	=	[2, 1]	list-extension(pair)	=	Lex
prec(fst)	=	2	status(fst)	=	[1]	list-extension(fst)	=	Lex
prec(natsFrom)	=	3	status(natsFrom)	=	[]	list-extension(natsFrom)	=	Lex
prec(a__snd)	=	2	status(a__snd)	=	[1]	list-extension(a__snd)	=	Lex
prec(splitAt)	=	5	status(splitAt)	=	[]	list-extension(splitAt)	=	Lex
prec(a__take^#)	=	0	status(a__take^#)	=	[1]	list-extension(a__take^#)	=	Lex
prec(a__natsFrom)	=	3	status(a__natsFrom)	=	[]	list-extension(a__natsFrom)	=	Lex
prec(a__fst)	=	2	status(a__fst)	=	[1]	list-extension(a__fst)	=	Lex
prec(tail)	=	2	status(tail)	=	[]	list-extension(tail)	=	Lex
prec(mark^#)	=	0	status(mark^#)	=	[]	list-extension(mark^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(a__u)	=	3	status(a__u)	=	[4]	list-extension(a__u)	=	Lex
prec(sel)	=	7	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(afterNth)	=	6	status(afterNth)	=	[]	list-extension(afterNth)	=	Lex
prec(nil)	=	6	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(a__splitAt)	=	5	status(a__splitAt)	=	[]	list-extension(a__splitAt)	=	Lex
prec(a__sel^#)	=	0	status(a__sel^#)	=	[1, 2]	list-extension(a__sel^#)	=	Lex
prec(a__sel)	=	7	status(a__sel)	=	[]	list-extension(a__sel)	=	Lex
prec(head)	=	7	status(head)	=	[]	list-extension(head)	=	Lex
prec(a__afterNth^#)	=	0	status(a__afterNth^#)	=	[1, 2]	list-extension(a__afterNth^#)	=	Lex
prec(a__splitAt^#)	=	0	status(a__splitAt^#)	=	[1]	list-extension(a__splitAt^#)	=	Lex
prec(cons)	=	1	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(snd)	=	2	status(snd)	=	[1]	list-extension(snd)	=	Lex
prec(a__u^#)	=	0	status(a__u^#)	=	[]	list-extension(a__u^#)	=	Lex
prec(a__take)	=	6	status(a__take)	=	[]	list-extension(a__take)	=	Lex
prec(a__fst^#)	=	0	status(a__fst^#)	=	[]	list-extension(a__fst^#)	=	Lex
prec(a__tail)	=	2	status(a__tail)	=	[]	list-extension(a__tail)	=	Lex
prec(a__tail^#)	=	0	status(a__tail^#)	=	[]	list-extension(a__tail^#)	=	Lex
prec(a__head)	=	7	status(a__head)	=	[]	list-extension(a__head)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[a__head^#(x₁)]	=	1
[a__snd^#(x₁)]	=	1
[a__afterNth(x₁, x₂)]	=	x₂ + 34525
[u(x₁,...,x₄)]	=	max(x₁ + 0, x₃ + 8, x₄ + 1, 0)
[take(x₁, x₂)]	=	x₂ + 7
[pair(x₁, x₂)]	=	max(x₁ + 3, x₂ + 2, 0)
[fst(x₁)]	=	x₁ + 1
[natsFrom(x₁)]	=	x₁ + 2451
[a__snd(x₁)]	=	x₁ + 32279
[splitAt(x₁, x₂)]	=	x₂ + 5
[a__take^#(x₁, x₂)]	=	x₁ + 1
[a__natsFrom(x₁)]	=	x₁ + 2451
[a__fst(x₁)]	=	x₁ + 1
[tail(x₁)]	=	x₁ + 1324
[mark^#(x₁)]	=	1
[0]	=	28886
[a__u(x₁,...,x₄)]	=	max(x₁ + 0, x₃ + 8, x₄ + 1, 0)
[sel(x₁, x₂)]	=	x₂ + 44252
[afterNth(x₁, x₂)]	=	x₂ + 34525
[nil]	=	1
[a__splitAt(x₁, x₂)]	=	x₂ + 5
[a__sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[a__sel(x₁, x₂)]	=	x₂ + 44252
[head(x₁)]	=	x₁ + 9726
[a__afterNth^#(x₁, x₂)]	=	x₁ + x₂ + 1
[a__splitAt^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 4, x₂ + 0, 0)
[snd(x₁)]	=	x₁ + 32279
[a__u^#(x₁,...,x₄)]	=	x₃ + 1
[a__take(x₁, x₂)]	=	x₂ + 7
[a__fst^#(x₁)]	=	1
[a__tail(x₁)]	=	x₁ + 1324
[a__tail^#(x₁)]	=	1
[a__head(x₁)]	=	x₁ + 9726

together with the usable rules

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

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

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

→

a__splitAt^#(mark(N),mark(XS))

(60)

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^#(u(X1,X2,X3,X4))	→	mark^#(X1)	(38)
mark^#(s(X))	→	mark^#(X)	(81)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[a__head^#(x₁)]	=	1
[a__natsFrom^#(x₁)]	=	0
[a__snd^#(x₁)]	=	0
[a__afterNth(x₁, x₂)]	=	1
[u(x₁,...,x₄)]	=	x₁ + 2
[take(x₁, x₂)]	=	2
[pair(x₁, x₂)]	=	5
[fst(x₁)]	=	5
[natsFrom(x₁)]	=	5
[a__snd(x₁)]	=	2
[splitAt(x₁, x₂)]	=	x₁ + 5
[a__take^#(x₁, x₂)]	=	0
[a__natsFrom(x₁)]	=	4
[a__fst(x₁)]	=	4
[tail(x₁)]	=	x₁ + 3
[mark^#(x₁)]	=	x₁ + 0
[0]	=	4
[a__u(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 1
[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__sel(x₁, x₂)]	=	x₂ + 1
[head(x₁)]	=	x₁ + 5
[a__afterNth^#(x₁, x₂)]	=	0
[a__splitAt^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₁ + 2
[snd(x₁)]	=	x₁ + 3
[a__u^#(x₁,...,x₄)]	=	0
[a__take(x₁, x₂)]	=	x₂ + 1
[a__fst^#(x₁)]	=	0
[a__tail(x₁)]	=	2
[a__tail^#(x₁)]	=	1
[a__head(x₁)]	=	4

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

mark^#(u(X1,X2,X3,X4))	→	mark^#(X1)	(38)
mark^#(s(X))	→	mark^#(X)	(81)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.