Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nosorts_C)

The rewrite relation of the following TRS is considered.

active(U11(tt,N,X,XS))	→	mark(U12(splitAt(N,XS),X))	(1)
active(U12(pair(YS,ZS),X))	→	mark(pair(cons(X,YS),ZS))	(2)
active(afterNth(N,XS))	→	mark(snd(splitAt(N,XS)))	(3)
active(and(tt,X))	→	mark(X)	(4)
active(fst(pair(X,Y)))	→	mark(X)	(5)
active(head(cons(N,XS)))	→	mark(N)	(6)
active(natsFrom(N))	→	mark(cons(N,natsFrom(s(N))))	(7)
active(sel(N,XS))	→	mark(head(afterNth(N,XS)))	(8)
active(snd(pair(X,Y)))	→	mark(Y)	(9)
active(splitAt(0,XS))	→	mark(pair(nil,XS))	(10)
active(splitAt(s(N),cons(X,XS)))	→	mark(U11(tt,N,X,XS))	(11)
active(tail(cons(N,XS)))	→	mark(XS)	(12)
active(take(N,XS))	→	mark(fst(splitAt(N,XS)))	(13)
active(U11(X1,X2,X3,X4))	→	U11(active(X1),X2,X3,X4)	(14)
active(U12(X1,X2))	→	U12(active(X1),X2)	(15)
active(splitAt(X1,X2))	→	splitAt(active(X1),X2)	(16)
active(splitAt(X1,X2))	→	splitAt(X1,active(X2))	(17)
active(pair(X1,X2))	→	pair(active(X1),X2)	(18)
active(pair(X1,X2))	→	pair(X1,active(X2))	(19)
active(cons(X1,X2))	→	cons(active(X1),X2)	(20)
active(afterNth(X1,X2))	→	afterNth(active(X1),X2)	(21)
active(afterNth(X1,X2))	→	afterNth(X1,active(X2))	(22)
active(snd(X))	→	snd(active(X))	(23)
active(and(X1,X2))	→	and(active(X1),X2)	(24)
active(fst(X))	→	fst(active(X))	(25)
active(head(X))	→	head(active(X))	(26)
active(natsFrom(X))	→	natsFrom(active(X))	(27)
active(s(X))	→	s(active(X))	(28)
active(sel(X1,X2))	→	sel(active(X1),X2)	(29)
active(sel(X1,X2))	→	sel(X1,active(X2))	(30)
active(tail(X))	→	tail(active(X))	(31)
active(take(X1,X2))	→	take(active(X1),X2)	(32)
active(take(X1,X2))	→	take(X1,active(X2))	(33)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(38)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(39)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(40)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
snd(mark(X))	→	mark(snd(X))	(43)
and(mark(X1),X2)	→	mark(and(X1,X2))	(44)
fst(mark(X))	→	mark(fst(X))	(45)
head(mark(X))	→	mark(head(X))	(46)
natsFrom(mark(X))	→	mark(natsFrom(X))	(47)
s(mark(X))	→	mark(s(X))	(48)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(49)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(50)
tail(mark(X))	→	mark(tail(X))	(51)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
proper(U11(X1,X2,X3,X4))	→	U11(proper(X1),proper(X2),proper(X3),proper(X4))	(54)
proper(tt)	→	ok(tt)	(55)
proper(U12(X1,X2))	→	U12(proper(X1),proper(X2))	(56)
proper(splitAt(X1,X2))	→	splitAt(proper(X1),proper(X2))	(57)
proper(pair(X1,X2))	→	pair(proper(X1),proper(X2))	(58)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(59)
proper(afterNth(X1,X2))	→	afterNth(proper(X1),proper(X2))	(60)
proper(snd(X))	→	snd(proper(X))	(61)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(62)
proper(fst(X))	→	fst(proper(X))	(63)
proper(head(X))	→	head(proper(X))	(64)
proper(natsFrom(X))	→	natsFrom(proper(X))	(65)
proper(s(X))	→	s(proper(X))	(66)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(67)
proper(0)	→	ok(0)	(68)
proper(nil)	→	ok(nil)	(69)
proper(tail(X))	→	tail(proper(X))	(70)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(71)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(75)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(76)
afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
snd(ok(X))	→	ok(snd(X))	(78)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(79)
fst(ok(X))	→	ok(fst(X))	(80)
head(ok(X))	→	ok(head(X))	(81)
natsFrom(ok(X))	→	ok(natsFrom(X))	(82)
s(ok(X))	→	ok(s(X))	(83)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(84)
tail(ok(X))	→	ok(tail(X))	(85)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)
top(mark(X))	→	top(proper(X))	(87)
top(ok(X))	→	top(active(X))	(88)

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.

There are 135 ruless (increase limit for explicit display).

1.1 Dependency Graph Processor

The dependency pairs are split into 18 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(114)
top^#(mark(X))	→	top^#(proper(X))	(99)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(fst)	=	1
π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(tail^#)	=	1
π(splitAt^#)	=	1
π(proper^#)	=	1
π(active)	=	1
π(head)	=	1

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

prec(U11)	=	5	status(U11)	=	[2, 4, 3, 1]	list-extension(U11)	=	Lex
prec(cons^#)	=	0	status(cons^#)	=	[]	list-extension(cons^#)	=	Lex
prec(s)	=	7	status(s)	=	[1]	list-extension(s)	=	Lex
prec(take^#)	=	0	status(take^#)	=	[1, 2]	list-extension(take^#)	=	Lex
prec(take)	=	3	status(take)	=	[2, 1]	list-extension(take)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(and)	=	3	status(and)	=	[2, 1]	list-extension(and)	=	Lex
prec(pair)	=	2	status(pair)	=	[1, 2]	list-extension(pair)	=	Lex
prec(natsFrom)	=	7	status(natsFrom)	=	[1]	list-extension(natsFrom)	=	Lex
prec(head^#)	=	0	status(head^#)	=	[]	list-extension(head^#)	=	Lex
prec(splitAt)	=	5	status(splitAt)	=	[1, 2]	list-extension(splitAt)	=	Lex
prec(fst^#)	=	0	status(fst^#)	=	[]	list-extension(fst^#)	=	Lex
prec(U12)	=	4	status(U12)	=	[1]	list-extension(U12)	=	Lex
prec(U12^#)	=	0	status(U12^#)	=	[2, 1]	list-extension(U12^#)	=	Lex
prec(tail)	=	7	status(tail)	=	[1]	list-extension(tail)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[1, 2]	list-extension(sel^#)	=	Lex
prec(sel)	=	8	status(sel)	=	[2, 1]	list-extension(sel)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(afterNth)	=	5	status(afterNth)	=	[2, 1]	list-extension(afterNth)	=	Lex
prec(nil)	=	6	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(mark)	=	1	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(afterNth^#)	=	0	status(afterNth^#)	=	[2, 1]	list-extension(afterNth^#)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[4, 3, 2, 1]	list-extension(U11^#)	=	Lex
prec(snd^#)	=	0	status(snd^#)	=	[]	list-extension(snd^#)	=	Lex
prec(cons)	=	3	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(natsFrom^#)	=	0	status(natsFrom^#)	=	[]	list-extension(natsFrom^#)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(snd)	=	3	status(snd)	=	[1]	list-extension(snd)	=	Lex
prec(tt)	=	8	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(pair^#)	=	0	status(pair^#)	=	[2, 1]	list-extension(pair^#)	=	Lex
prec(and^#)	=	0	status(and^#)	=	[1, 2]	list-extension(and^#)	=	Lex

and the following Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	max(x₁ + 58818, x₂ + 29411, x₃ + 29410, x₄ + 58817, 0)
[cons^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	x₁ + x₂ + 1
[take(x₁, x₂)]	=	x₁ + x₂ + 66447
[top(x₁)]	=	1
[and(x₁, x₂)]	=	x₁ + x₂ + 11650
[pair(x₁, x₂)]	=	max(x₁ + 29407, x₂ + 29407, 0)
[natsFrom(x₁)]	=	x₁ + 12282
[head^#(x₁)]	=	1
[splitAt(x₁, x₂)]	=	max(x₁ + 29411, x₂ + 58817, 0)
[fst^#(x₁)]	=	1
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 29410, 0)
[U12^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[tail(x₁)]	=	x₁ + 13506
[0]	=	29408
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 83208
[s^#(x₁)]	=	1
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 83207
[nil]	=	29409
[mark(x₁)]	=	x₁ + 0
[afterNth^#(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁,...,x₄)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, x₄ + 1, 0)
[snd^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[natsFrom^#(x₁)]	=	1
[active^#(x₁)]	=	1
[snd(x₁)]	=	x₁ + 24389
[tt]	=	1
[pair^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[and^#(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

active(pair(X1,X2))	→	pair(active(X1),X2)	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(50)
fst(ok(X))	→	ok(fst(X))	(80)
active(and(tt,X))	→	mark(X)	(4)
active(U12(X1,X2))	→	U12(active(X1),X2)	(15)
active(sel(N,XS))	→	mark(head(afterNth(N,XS)))	(8)
proper(U11(X1,X2,X3,X4))	→	U11(proper(X1),proper(X2),proper(X3),proper(X4))	(54)
active(U11(tt,N,X,XS))	→	mark(U12(splitAt(N,XS),X))	(1)
afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
active(afterNth(N,XS))	→	mark(snd(splitAt(N,XS)))	(3)
active(splitAt(X1,X2))	→	splitAt(active(X1),X2)	(16)
active(afterNth(X1,X2))	→	afterNth(active(X1),X2)	(21)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
proper(0)	→	ok(0)	(68)
tail(ok(X))	→	ok(tail(X))	(85)
active(head(X))	→	head(active(X))	(26)
proper(fst(X))	→	fst(proper(X))	(63)
active(pair(X1,X2))	→	pair(X1,active(X2))	(19)
active(take(X1,X2))	→	take(active(X1),X2)	(32)
active(splitAt(X1,X2))	→	splitAt(X1,active(X2))	(17)
proper(afterNth(X1,X2))	→	afterNth(proper(X1),proper(X2))	(60)
active(natsFrom(X))	→	natsFrom(active(X))	(27)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(84)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
active(afterNth(X1,X2))	→	afterNth(X1,active(X2))	(22)
active(s(X))	→	s(active(X))	(28)
proper(natsFrom(X))	→	natsFrom(proper(X))	(65)
and(mark(X1),X2)	→	mark(and(X1,X2))	(44)
active(fst(pair(X,Y)))	→	mark(X)	(5)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
active(take(X1,X2))	→	take(X1,active(X2))	(33)
proper(head(X))	→	head(proper(X))	(64)
active(splitAt(0,XS))	→	mark(pair(nil,XS))	(10)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(39)
active(natsFrom(N))	→	mark(cons(N,natsFrom(s(N))))	(7)
active(cons(X1,X2))	→	cons(active(X1),X2)	(20)
active(fst(X))	→	fst(active(X))	(25)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(49)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
active(sel(X1,X2))	→	sel(X1,active(X2))	(30)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(62)
active(U11(X1,X2,X3,X4))	→	U11(active(X1),X2,X3,X4)	(14)
natsFrom(ok(X))	→	ok(natsFrom(X))	(82)
proper(U12(X1,X2))	→	U12(proper(X1),proper(X2))	(56)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(79)
active(tail(X))	→	tail(active(X))	(31)
active(tail(cons(N,XS)))	→	mark(XS)	(12)
proper(nil)	→	ok(nil)	(69)
fst(mark(X))	→	mark(fst(X))	(45)
snd(ok(X))	→	ok(snd(X))	(78)
head(ok(X))	→	ok(head(X))	(81)
active(snd(X))	→	snd(active(X))	(23)
proper(tail(X))	→	tail(proper(X))	(70)
active(and(X1,X2))	→	and(active(X1),X2)	(24)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(76)
proper(splitAt(X1,X2))	→	splitAt(proper(X1),proper(X2))	(57)
active(splitAt(s(N),cons(X,XS)))	→	mark(U11(tt,N,X,XS))	(11)
active(snd(pair(X,Y)))	→	mark(Y)	(9)
active(take(N,XS))	→	mark(fst(splitAt(N,XS)))	(13)
tail(mark(X))	→	mark(tail(X))	(51)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(40)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(67)
proper(tt)	→	ok(tt)	(55)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(59)
active(head(cons(N,XS)))	→	mark(N)	(6)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(38)
proper(snd(X))	→	snd(proper(X))	(61)
proper(pair(X1,X2))	→	pair(proper(X1),proper(X2))	(58)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(75)
s(mark(X))	→	mark(s(X))	(48)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(71)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
natsFrom(mark(X))	→	mark(natsFrom(X))	(47)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
head(mark(X))	→	mark(head(X))	(46)
proper(s(X))	→	s(proper(X))	(66)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
active(sel(X1,X2))	→	sel(active(X1),X2)	(29)
snd(mark(X))	→	mark(snd(X))	(43)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)
active(U12(pair(YS,ZS),X))	→	mark(pair(cons(X,YS),ZS))	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(99)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

top^#(ok(X))

→

top^#(active(X))

(114)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₃ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 0
[pair(x₁, x₂)]	=	x₁ + 0
[fst(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	x₁ + 0
[natsFrom(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₂ + 0
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 0
[proper(x₁)]	=	3
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + 0
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	x₂ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	0
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	x₁ + 1
[head(x₁)]	=	x₁ + 0
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 0
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	x₁ + 0
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

active(pair(X1,X2))	→	pair(active(X1),X2)	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(50)
fst(ok(X))	→	ok(fst(X))	(80)
active(and(tt,X))	→	mark(X)	(4)
active(U12(X1,X2))	→	U12(active(X1),X2)	(15)
active(sel(N,XS))	→	mark(head(afterNth(N,XS)))	(8)
proper(U11(X1,X2,X3,X4))	→	U11(proper(X1),proper(X2),proper(X3),proper(X4))	(54)
active(U11(tt,N,X,XS))	→	mark(U12(splitAt(N,XS),X))	(1)
afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
active(afterNth(N,XS))	→	mark(snd(splitAt(N,XS)))	(3)
active(splitAt(X1,X2))	→	splitAt(active(X1),X2)	(16)
active(afterNth(X1,X2))	→	afterNth(active(X1),X2)	(21)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
proper(0)	→	ok(0)	(68)
tail(ok(X))	→	ok(tail(X))	(85)
active(head(X))	→	head(active(X))	(26)
proper(fst(X))	→	fst(proper(X))	(63)
active(pair(X1,X2))	→	pair(X1,active(X2))	(19)
active(take(X1,X2))	→	take(active(X1),X2)	(32)
active(splitAt(X1,X2))	→	splitAt(X1,active(X2))	(17)
proper(afterNth(X1,X2))	→	afterNth(proper(X1),proper(X2))	(60)
active(natsFrom(X))	→	natsFrom(active(X))	(27)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(84)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
active(afterNth(X1,X2))	→	afterNth(X1,active(X2))	(22)
active(s(X))	→	s(active(X))	(28)
proper(natsFrom(X))	→	natsFrom(proper(X))	(65)
and(mark(X1),X2)	→	mark(and(X1,X2))	(44)
active(fst(pair(X,Y)))	→	mark(X)	(5)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
active(take(X1,X2))	→	take(X1,active(X2))	(33)
proper(head(X))	→	head(proper(X))	(64)
active(splitAt(0,XS))	→	mark(pair(nil,XS))	(10)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(39)
active(natsFrom(N))	→	mark(cons(N,natsFrom(s(N))))	(7)
active(cons(X1,X2))	→	cons(active(X1),X2)	(20)
active(fst(X))	→	fst(active(X))	(25)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(49)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
active(sel(X1,X2))	→	sel(X1,active(X2))	(30)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(62)
active(U11(X1,X2,X3,X4))	→	U11(active(X1),X2,X3,X4)	(14)
natsFrom(ok(X))	→	ok(natsFrom(X))	(82)
proper(U12(X1,X2))	→	U12(proper(X1),proper(X2))	(56)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(79)
active(tail(X))	→	tail(active(X))	(31)
active(tail(cons(N,XS)))	→	mark(XS)	(12)
proper(nil)	→	ok(nil)	(69)
fst(mark(X))	→	mark(fst(X))	(45)
snd(ok(X))	→	ok(snd(X))	(78)
head(ok(X))	→	ok(head(X))	(81)
active(snd(X))	→	snd(active(X))	(23)
proper(tail(X))	→	tail(proper(X))	(70)
active(and(X1,X2))	→	and(active(X1),X2)	(24)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(76)
proper(splitAt(X1,X2))	→	splitAt(proper(X1),proper(X2))	(57)
active(splitAt(s(N),cons(X,XS)))	→	mark(U11(tt,N,X,XS))	(11)
active(snd(pair(X,Y)))	→	mark(Y)	(9)
active(take(N,XS))	→	mark(fst(splitAt(N,XS)))	(13)
tail(mark(X))	→	mark(tail(X))	(51)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(40)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(67)
proper(tt)	→	ok(tt)	(55)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(59)
active(head(cons(N,XS)))	→	mark(N)	(6)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(38)
proper(snd(X))	→	snd(proper(X))	(61)
proper(pair(X1,X2))	→	pair(proper(X1),proper(X2))	(58)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(75)
s(mark(X))	→	mark(s(X))	(48)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(71)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
natsFrom(mark(X))	→	mark(natsFrom(X))	(47)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
head(mark(X))	→	mark(head(X))	(46)
proper(s(X))	→	s(proper(X))	(66)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
active(sel(X1,X2))	→	sel(active(X1),X2)	(29)
snd(mark(X))	→	mark(snd(X))	(43)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)
active(U12(pair(YS,ZS),X))	→	mark(pair(cons(X,YS),ZS))	(2)

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

top^#(ok(X))

→

top^#(active(X))

(114)

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

active^#(snd(X))	→	active^#(X)	(222)
active^#(U11(X1,X2,X3,X4))	→	active^#(X1)	(160)
active^#(splitAt(X1,X2))	→	active^#(X2)	(218)
active^#(head(X))	→	active^#(X)	(157)
active^#(U12(X1,X2))	→	active^#(X1)	(205)
active^#(natsFrom(X))	→	active^#(X)	(133)
active^#(take(X1,X2))	→	active^#(X1)	(199)
active^#(pair(X1,X2))	→	active^#(X1)	(198)
active^#(pair(X1,X2))	→	active^#(X2)	(128)
active^#(s(X))	→	active^#(X)	(127)
active^#(sel(X1,X2))	→	active^#(X2)	(125)
active^#(tail(X))	→	active^#(X)	(124)
active^#(splitAt(X1,X2))	→	active^#(X1)	(192)
active^#(sel(X1,X2))	→	active^#(X1)	(120)
active^#(take(X1,X2))	→	active^#(X2)	(188)
active^#(fst(X))	→	active^#(X)	(109)
active^#(cons(X1,X2))	→	active^#(X1)	(106)
active^#(afterNth(X1,X2))	→	active^#(X1)	(98)
active^#(afterNth(X1,X2))	→	active^#(X2)	(174)
active^#(and(X1,X2))	→	active^#(X1)	(96)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₃ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[fst(x₁)]	=	x₁ + 1
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 5082
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₁ + x₂ + 1
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + 1
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 24897
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	3
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 1
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 0
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	0
[head(x₁)]	=	x₁ + 1
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	x₁ + 0
[snd(x₁)]	=	x₁ + 1
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
s(mark(X))	→	mark(s(X))	(48)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)

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

active^#(snd(X))	→	active^#(X)	(222)
active^#(U11(X1,X2,X3,X4))	→	active^#(X1)	(160)
active^#(splitAt(X1,X2))	→	active^#(X2)	(218)
active^#(head(X))	→	active^#(X)	(157)
active^#(U12(X1,X2))	→	active^#(X1)	(205)
active^#(natsFrom(X))	→	active^#(X)	(133)
active^#(take(X1,X2))	→	active^#(X1)	(199)
active^#(pair(X1,X2))	→	active^#(X1)	(198)
active^#(pair(X1,X2))	→	active^#(X2)	(128)
active^#(s(X))	→	active^#(X)	(127)
active^#(sel(X1,X2))	→	active^#(X2)	(125)
active^#(tail(X))	→	active^#(X)	(124)
active^#(splitAt(X1,X2))	→	active^#(X1)	(192)
active^#(sel(X1,X2))	→	active^#(X1)	(120)
active^#(take(X1,X2))	→	active^#(X2)	(188)
active^#(fst(X))	→	active^#(X)	(109)
active^#(cons(X1,X2))	→	active^#(X1)	(106)
active^#(afterNth(X1,X2))	→	active^#(X1)	(98)
active^#(afterNth(X1,X2))	→	active^#(X2)	(174)
active^#(and(X1,X2))	→	active^#(X1)	(96)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

proper^#(pair(X1,X2))	→	proper^#(X1)	(164)
proper^#(head(X))	→	proper^#(X)	(156)
proper^#(cons(X1,X2))	→	proper^#(X1)	(151)
proper^#(afterNth(X1,X2))	→	proper^#(X2)	(149)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X1)	(212)
proper^#(fst(X))	→	proper^#(X)	(136)
proper^#(afterNth(X1,X2))	→	proper^#(X1)	(201)
proper^#(pair(X1,X2))	→	proper^#(X2)	(200)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X2)	(196)
proper^#(cons(X1,X2))	→	proper^#(X2)	(194)
proper^#(take(X1,X2))	→	proper^#(X1)	(195)
proper^#(U12(X1,X2))	→	proper^#(X2)	(121)
proper^#(U12(X1,X2))	→	proper^#(X1)	(115)
proper^#(sel(X1,X2))	→	proper^#(X1)	(187)
proper^#(tail(X))	→	proper^#(X)	(110)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X4)	(186)
proper^#(snd(X))	→	proper^#(X)	(184)
proper^#(and(X1,X2))	→	proper^#(X2)	(183)
proper^#(and(X1,X2))	→	proper^#(X1)	(177)
proper^#(splitAt(X1,X2))	→	proper^#(X1)	(97)
proper^#(s(X))	→	proper^#(X)	(173)
proper^#(natsFrom(X))	→	proper^#(X)	(170)
proper^#(sel(X1,X2))	→	proper^#(X2)	(93)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X3)	(169)
proper^#(splitAt(X1,X2))	→	proper^#(X2)	(91)
proper^#(take(X1,X2))	→	proper^#(X2)	(168)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[fst(x₁)]	=	x₁ + 1
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₁ + x₂ + 1
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 24897
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 1
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 0
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	x₁ + 0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	0
[head(x₁)]	=	x₁ + 1
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	x₁ + 1
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
s(mark(X))	→	mark(s(X))	(48)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)

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

proper^#(pair(X1,X2))	→	proper^#(X1)	(164)
proper^#(head(X))	→	proper^#(X)	(156)
proper^#(cons(X1,X2))	→	proper^#(X1)	(151)
proper^#(afterNth(X1,X2))	→	proper^#(X2)	(149)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X1)	(212)
proper^#(fst(X))	→	proper^#(X)	(136)
proper^#(afterNth(X1,X2))	→	proper^#(X1)	(201)
proper^#(pair(X1,X2))	→	proper^#(X2)	(200)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X2)	(196)
proper^#(cons(X1,X2))	→	proper^#(X2)	(194)
proper^#(take(X1,X2))	→	proper^#(X1)	(195)
proper^#(U12(X1,X2))	→	proper^#(X2)	(121)
proper^#(U12(X1,X2))	→	proper^#(X1)	(115)
proper^#(sel(X1,X2))	→	proper^#(X1)	(187)
proper^#(tail(X))	→	proper^#(X)	(110)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X4)	(186)
proper^#(snd(X))	→	proper^#(X)	(184)
proper^#(and(X1,X2))	→	proper^#(X2)	(183)
proper^#(and(X1,X2))	→	proper^#(X1)	(177)
proper^#(splitAt(X1,X2))	→	proper^#(X1)	(97)
proper^#(s(X))	→	proper^#(X)	(173)
proper^#(natsFrom(X))	→	proper^#(X)	(170)
proper^#(sel(X1,X2))	→	proper^#(X2)	(93)
proper^#(U11(X1,X2,X3,X4))	→	proper^#(X3)	(169)
proper^#(splitAt(X1,X2))	→	proper^#(X2)	(91)
proper^#(take(X1,X2))	→	proper^#(X2)	(168)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

s^#(ok(X))	→	s^#(X)	(214)
s^#(mark(X))	→	s^#(X)	(207)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[fst(x₁)]	=	x₁ + 1
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₁ + x₂ + 1
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	x₁ + 0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 0
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	0
[head(x₁)]	=	x₁ + 1
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	x₁ + 1
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
s(mark(X))	→	mark(s(X))	(48)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)

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

s^#(ok(X))

→

s^#(X)

(214)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

s^#(mark(X))

→

s^#(X)

(207)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[pair(x₁, x₂)]	=	x₁ + x₂ + 21807
[fst(x₁)]	=	4337
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₂ + 2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + x₂ + 6911
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 29094
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 21208
[s^#(x₁)]	=	x₁ + 0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 10113
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	x₁ + 12620
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
s(mark(X))	→	mark(s(X))	(48)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)

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

s^#(mark(X))

→

s^#(X)

(207)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(209)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(204)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(193)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	x₂ + 0
[take(x₁, x₂)]	=	x₁ + x₂ + 0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 22305
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[fst(x₁)]	=	28224
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₂ + 2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 34320
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	x₁ + 1
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
s(mark(X))	→	mark(s(X))	(48)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)

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

take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(209)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(193)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

take^#(mark(X1),X2)

→

take^#(X1,X2)

(204)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	x₁ + 0
[take(x₁, x₂)]	=	x₁ + x₂ + 0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[fst(x₁)]	=	5581
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	x₁ + x₂ + 25150
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₁ + x₂ + 1
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 32467
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 24235
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	x₁ + 1
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

afterNth(ok(X1),ok(X2))	→	ok(afterNth(X1,X2))	(77)
splitAt(mark(X1),X2)	→	mark(splitAt(X1,X2))	(36)
U11(mark(X1),X2,X3,X4)	→	mark(U11(X1,X2,X3,X4))	(34)
U11(ok(X1),ok(X2),ok(X3),ok(X4))	→	ok(U11(X1,X2,X3,X4))	(72)
take(mark(X1),X2)	→	mark(take(X1,X2))	(52)
splitAt(ok(X1),ok(X2))	→	ok(splitAt(X1,X2))	(74)
s(mark(X))	→	mark(s(X))	(48)
take(X1,mark(X2))	→	mark(take(X1,X2))	(53)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(73)
splitAt(X1,mark(X2))	→	mark(splitAt(X1,X2))	(37)
afterNth(mark(X1),X2)	→	mark(afterNth(X1,X2))	(41)
afterNth(X1,mark(X2))	→	mark(afterNth(X1,X2))	(42)
s(ok(X))	→	ok(s(X))	(83)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(35)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(86)

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

take^#(mark(X1),X2)

→

take^#(X1,X2)

(204)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(152)
pair^#(ok(X1),ok(X2))	→	pair^#(X1,X2)	(185)
pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(92)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₃ + 18698
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	616
[pair(x₁, x₂)]	=	x₂ + 24124
[fst(x₁)]	=	31048
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 37157
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	27127
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	23724
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	12771
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 29351
[0]	=	21965
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	18419
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	15079
[nil]	=	52813
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 7675
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	28473
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 24813
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	23033
[tt]	=	1
[pair^#(x₁, x₂)]	=	x₁ + x₂ + 0
[and^#(x₁, x₂)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(48)
s(ok(X))	→	ok(s(X))	(83)

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

pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(152)
pair^#(ok(X1),ok(X2))	→	pair^#(X1,X2)	(185)
pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(92)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

snd^#(ok(X))	→	snd^#(X)	(162)
snd^#(mark(X))	→	snd^#(X)	(219)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	25853
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	15786
[top(x₁)]	=	0
[and(x₁, x₂)]	=	31849
[pair(x₁, x₂)]	=	x₁ + 8927
[fst(x₁)]	=	19784
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	25324
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 22742
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	12876
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 764
[0]	=	56785
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	17272
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	16847
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 4
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	3
[head(x₁)]	=	12450
[snd^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 8930
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	23381
[tt]	=	4673
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

snd^#(ok(X))	→	snd^#(X)	(162)
snd^#(mark(X))	→	snd^#(X)	(219)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(206)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(182)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	25853
[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	12333
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	35596
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	16038
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 27469
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	12874
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	34659
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 39590
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	17083
[tt]	=	4673
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(206)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(182)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(155)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(148)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(137)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	10310
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 9623
[top(x₁)]	=	0
[and(x₁, x₂)]	=	32023
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	27135
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 17535
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	12874
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	x₂ + 0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	7943
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(155)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(137)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

sel^#(mark(X1),X2)

→

sel^#(X1,X2)

(148)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	11794
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	5599
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	4582
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 2
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	12874
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 28859
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + 0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	32359
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

sel^#(mark(X1),X2)

→

sel^#(X1,X2)

(148)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

splitAt^#(X1,mark(X2))	→	splitAt^#(X1,X2)	(158)
splitAt^#(ok(X1),ok(X2))	→	splitAt^#(X1,X2)	(141)
splitAt^#(mark(X1),X2)	→	splitAt^#(X1,X2)	(116)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	24036
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 22135
[top(x₁)]	=	0
[and(x₁, x₂)]	=	16349
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	12700
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 3449
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 2
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	12874
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	30145
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	52051
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	x₂ + 0
[mark(x₁)]	=	x₁ + 5
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	22051
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	18072
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

splitAt^#(X1,mark(X2))	→	splitAt^#(X1,X2)	(158)
splitAt^#(ok(X1),ok(X2))	→	splitAt^#(X1,X2)	(141)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

splitAt^#(mark(X1),X2)

→

splitAt^#(X1,X2)

(116)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	24036
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 19734
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	30435
[pair(x₁, x₂)]	=	x₁ + 6246
[fst(x₁)]	=	890
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 2
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 13507
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	30145
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 18407
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	18072
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

splitAt^#(mark(X1),X2)

→

splitAt^#(X1,X2)

(116)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

tail^#(ok(X))	→	tail^#(X)	(113)
tail^#(mark(X))	→	tail^#(X)	(101)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	5152
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 19734
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 25342
[top(x₁)]	=	0
[and(x₁, x₂)]	=	30435
[pair(x₁, x₂)]	=	x₁ + 3190
[fst(x₁)]	=	22295
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	5576
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 25320
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 27869
[0]	=	1090
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1751
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	29044
[nil]	=	19891
[tail^#(x₁)]	=	x₁ + 0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 18407
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	4811
[tt]	=	10509
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

tail^#(ok(X))	→	tail^#(X)	(113)
tail^#(mark(X))	→	tail^#(X)	(101)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 12^th component contains the pair

U12^#(ok(X1),ok(X2))	→	U12^#(X1,X2)	(216)
U12^#(mark(X1),X2)	→	U12^#(X1,X2)	(171)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	5152
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	30435
[pair(x₁, x₂)]	=	x₁ + 26107
[fst(x₁)]	=	2
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 30352
[U12^#(x₁, x₂)]	=	x₂ + 0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 4004
[0]	=	9311
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	22786
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	4811
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

U12^#(ok(X1),ok(X2))

→

U12^#(X1,X2)

(216)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U12^#(mark(X1),X2)

→

U12^#(X1,X2)

(171)

1.1.12.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	2
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 482
[top(x₁)]	=	0
[and(x₁, x₂)]	=	16560
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	2
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 24825
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 30895
[U12^#(x₁, x₂)]	=	x₁ + 0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	23490
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	19177
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

U12^#(mark(X1),X2)

→

U12^#(X1,X2)

(171)

could be deleted.

1.1.12.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 13^th component contains the pair

and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(153)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(90)

1.1.13 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	2
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 11875
[top(x₁)]	=	0
[and(x₁, x₂)]	=	7531
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	2
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 13881
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 16387
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 21559
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	x₁ + 0

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

and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(153)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(90)

could be deleted.

1.1.13.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 14^th component contains the pair

head^#(mark(X))	→	head^#(X)	(132)
head^#(ok(X))	→	head^#(X)	(129)

1.1.14 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	17267
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 32353
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 11875
[top(x₁)]	=	0
[and(x₁, x₂)]	=	8234
[pair(x₁, x₂)]	=	x₁ + 9543
[fst(x₁)]	=	10182
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	x₁ + 0
[splitAt(x₁, x₂)]	=	11765
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 42654
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 21559
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	26837
[nil]	=	11414
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	11804
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 19214
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	26537
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

head^#(mark(X))	→	head^#(X)	(132)
head^#(ok(X))	→	head^#(X)	(129)

could be deleted.

1.1.14.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 15^th component contains the pair

natsFrom^#(mark(X))	→	natsFrom^#(X)	(208)
natsFrom^#(ok(X))	→	natsFrom^#(X)	(191)

1.1.15 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	22101
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 32353
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 30530
[top(x₁)]	=	0
[and(x₁, x₂)]	=	8234
[pair(x₁, x₂)]	=	x₁ + 9607
[fst(x₁)]	=	2
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	11765
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 64240
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 4418
[0]	=	196
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	13579
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	26837
[nil]	=	57134
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 10741
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	25054
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 32537
[natsFrom^#(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	32207
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

natsFrom^#(mark(X))	→	natsFrom^#(X)	(208)
natsFrom^#(ok(X))	→	natsFrom^#(X)	(191)

could be deleted.

1.1.15.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 16^th component contains the pair

afterNth^#(X1,mark(X2))	→	afterNth^#(X1,X2)	(150)
afterNth^#(mark(X1),X2)	→	afterNth^#(X1,X2)	(130)
afterNth^#(ok(X1),ok(X2))	→	afterNth^#(X1,X2)	(180)

1.1.16 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	23655
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	2939
[pair(x₁, x₂)]	=	x₁ + 8742
[fst(x₁)]	=	2
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	2
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 64240
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 12881
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	13579
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 20987
[afterNth^#(x₁, x₂)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	32207
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

afterNth^#(mark(X1),X2)	→	afterNth^#(X1,X2)	(130)
afterNth^#(ok(X1),ok(X2))	→	afterNth^#(X1,X2)	(180)

could be deleted.

1.1.16.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

afterNth^#(X1,mark(X2))

→

afterNth^#(X1,X2)

(150)

1.1.16.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	2
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[and(x₁, x₂)]	=	2939
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	2
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	16521
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 88366
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 9911
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 31992
[afterNth^#(x₁, x₂)]	=	x₂ + 0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

afterNth^#(X1,mark(X2))

→

afterNth^#(X1,X2)

(150)

could be deleted.

1.1.16.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 17^th component contains the pair

fst^#(ok(X))	→	fst^#(X)	(123)
fst^#(mark(X))	→	fst^#(X)	(108)

1.1.17 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	15214
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 15343
[top(x₁)]	=	0
[and(x₁, x₂)]	=	20023
[pair(x₁, x₂)]	=	x₁ + 15062
[fst(x₁)]	=	17221
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	21762
[fst^#(x₁)]	=	x₁ + 0
[U12(x₁, x₂)]	=	x₂ + 117584
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 4390
[0]	=	20099
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	2
[nil]	=	2998
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 31992
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	13135
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 32435
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	2
[tt]	=	46716
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

fst^#(ok(X))	→	fst^#(X)	(123)
fst^#(mark(X))	→	fst^#(X)	(108)

could be deleted.

1.1.17.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 18^th component contains the pair

U11^#(ok(X1),ok(X2),ok(X3),ok(X4))	→	U11^#(X1,X2,X3,X4)	(202)
U11^#(mark(X1),X2,X3,X4)	→	U11^#(X1,X2,X3,X4)	(176)

1.1.18 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	2
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 23861
[top(x₁)]	=	0
[and(x₁, x₂)]	=	12572
[pair(x₁, x₂)]	=	x₁ + 2
[fst(x₁)]	=	47115
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 1
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	26412
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	x₂ + 2
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27345
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 834
[0]	=	94
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	30824
[nil]	=	1
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 2215
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	x₂ + 0
[active(x₁)]	=	1
[head(x₁)]	=	25940
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 15781
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	295
[tt]	=	16686
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

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

U11^#(ok(X1),ok(X2),ok(X3),ok(X4))

→

U11^#(X1,X2,X3,X4)

(202)

could be deleted.

1.1.18.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U11^#(mark(X1),X2,X3,X4)

→

U11^#(X1,X2,X3,X4)

(176)

1.1.18.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + x₄ + 18486
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	2
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	5795
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 47487
[pair(x₁, x₂)]	=	x₂ + 24318
[fst(x₁)]	=	7035
[top^#(x₁)]	=	0
[natsFrom(x₁)]	=	x₁ + 38236
[head^#(x₁)]	=	0
[splitAt(x₁, x₂)]	=	5823
[fst^#(x₁)]	=	0
[U12(x₁, x₂)]	=	17426
[U12^#(x₁, x₂)]	=	0
[tail(x₁)]	=	27631
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 18246
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 21797
[s^#(x₁)]	=	0
[afterNth(x₁, x₂)]	=	x₁ + x₂ + 1
[nil]	=	25783
[tail^#(x₁)]	=	0
[splitAt^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5967
[afterNth^#(x₁, x₂)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁,...,x₄)]	=	x₁ + 0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[snd^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + 1
[natsFrom^#(x₁)]	=	0
[active^#(x₁)]	=	0
[snd(x₁)]	=	27114
[tt]	=	1
[pair^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(50)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(84)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(49)

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

U11^#(mark(X1),X2,X3,X4)

→

U11^#(X1,X2,X3,X4)

(176)

could be deleted.

1.1.18.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.