Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_Luc02a_C)

The rewrite relation of the following TRS is considered.

active(terms(N))	→	mark(cons(recip(sqr(N)),terms(s(N))))	(1)
active(sqr(0))	→	mark(0)	(2)
active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
active(dbl(0))	→	mark(0)	(4)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
active(add(0,X))	→	mark(X)	(6)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
active(first(0,X))	→	mark(nil)	(8)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
active(half(0))	→	mark(0)	(10)
active(half(s(0)))	→	mark(0)	(11)
active(half(s(s(X))))	→	mark(s(half(X)))	(12)
active(half(dbl(X)))	→	mark(X)	(13)
active(terms(X))	→	terms(active(X))	(14)
active(cons(X1,X2))	→	cons(active(X1),X2)	(15)
active(recip(X))	→	recip(active(X))	(16)
active(sqr(X))	→	sqr(active(X))	(17)
active(s(X))	→	s(active(X))	(18)
active(add(X1,X2))	→	add(active(X1),X2)	(19)
active(add(X1,X2))	→	add(X1,active(X2))	(20)
active(dbl(X))	→	dbl(active(X))	(21)
active(first(X1,X2))	→	first(active(X1),X2)	(22)
active(first(X1,X2))	→	first(X1,active(X2))	(23)
active(half(X))	→	half(active(X))	(24)
terms(mark(X))	→	mark(terms(X))	(25)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(26)
recip(mark(X))	→	mark(recip(X))	(27)
sqr(mark(X))	→	mark(sqr(X))	(28)
s(mark(X))	→	mark(s(X))	(29)
add(mark(X1),X2)	→	mark(add(X1,X2))	(30)
add(X1,mark(X2))	→	mark(add(X1,X2))	(31)
dbl(mark(X))	→	mark(dbl(X))	(32)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
half(mark(X))	→	mark(half(X))	(35)
proper(terms(X))	→	terms(proper(X))	(36)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(37)
proper(recip(X))	→	recip(proper(X))	(38)
proper(sqr(X))	→	sqr(proper(X))	(39)
proper(s(X))	→	s(proper(X))	(40)
proper(0)	→	ok(0)	(41)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(42)
proper(dbl(X))	→	dbl(proper(X))	(43)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(44)
proper(nil)	→	ok(nil)	(45)
proper(half(X))	→	half(proper(X))	(46)
terms(ok(X))	→	ok(terms(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(48)
recip(ok(X))	→	ok(recip(X))	(49)
sqr(ok(X))	→	ok(sqr(X))	(50)
s(ok(X))	→	ok(s(X))	(51)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
dbl(ok(X))	→	ok(dbl(X))	(53)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
half(ok(X))	→	ok(half(X))	(55)
top(mark(X))	→	top(proper(X))	(56)
top(ok(X))	→	top(active(X))	(57)

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.

proper^#(dbl(X))	→	proper^#(X)	(58)
active^#(add(s(X),Y))	→	s^#(add(X,Y))	(59)
active^#(first(X1,X2))	→	active^#(X2)	(60)
active^#(terms(X))	→	terms^#(active(X))	(61)
sqr^#(ok(X))	→	sqr^#(X)	(62)
proper^#(terms(X))	→	proper^#(X)	(63)
proper^#(sqr(X))	→	proper^#(X)	(64)
active^#(add(X1,X2))	→	active^#(X2)	(65)
active^#(add(X1,X2))	→	add^#(X1,active(X2))	(66)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(67)
active^#(sqr(s(X)))	→	sqr^#(X)	(68)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(69)
proper^#(first(X1,X2))	→	proper^#(X2)	(70)
active^#(sqr(s(X)))	→	s^#(add(sqr(X),dbl(X)))	(71)
active^#(dbl(s(X)))	→	s^#(s(dbl(X)))	(72)
active^#(terms(N))	→	cons^#(recip(sqr(N)),terms(s(N)))	(73)
active^#(sqr(s(X)))	→	dbl^#(X)	(74)
recip^#(mark(X))	→	recip^#(X)	(75)
dbl^#(mark(X))	→	dbl^#(X)	(76)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(77)
proper^#(half(X))	→	proper^#(X)	(78)
active^#(sqr(X))	→	sqr^#(active(X))	(79)
active^#(first(X1,X2))	→	first^#(active(X1),X2)	(80)
active^#(dbl(X))	→	dbl^#(active(X))	(81)
terms^#(mark(X))	→	terms^#(X)	(82)
proper^#(first(X1,X2))	→	first^#(proper(X1),proper(X2))	(83)
terms^#(ok(X))	→	terms^#(X)	(84)
proper^#(add(X1,X2))	→	proper^#(X2)	(85)
proper^#(cons(X1,X2))	→	proper^#(X1)	(86)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(87)
active^#(terms(N))	→	recip^#(sqr(N))	(88)
top^#(ok(X))	→	top^#(active(X))	(89)
active^#(recip(X))	→	active^#(X)	(90)
active^#(first(s(X),cons(Y,Z)))	→	first^#(X,Z)	(91)
active^#(cons(X1,X2))	→	cons^#(active(X1),X2)	(92)
active^#(terms(N))	→	terms^#(s(N))	(93)
proper^#(sqr(X))	→	sqr^#(proper(X))	(94)
active^#(recip(X))	→	recip^#(active(X))	(95)
proper^#(cons(X1,X2))	→	proper^#(X2)	(96)
active^#(half(s(s(X))))	→	half^#(X)	(97)
active^#(terms(N))	→	s^#(N)	(98)
active^#(first(X1,X2))	→	active^#(X1)	(99)
active^#(cons(X1,X2))	→	active^#(X1)	(100)
dbl^#(ok(X))	→	dbl^#(X)	(101)
active^#(add(X1,X2))	→	add^#(active(X1),X2)	(102)
active^#(half(s(s(X))))	→	s^#(half(X))	(103)
proper^#(first(X1,X2))	→	proper^#(X1)	(104)
active^#(dbl(s(X)))	→	s^#(dbl(X))	(105)
top^#(ok(X))	→	active^#(X)	(106)
proper^#(s(X))	→	proper^#(X)	(107)
proper^#(add(X1,X2))	→	add^#(proper(X1),proper(X2))	(108)
recip^#(ok(X))	→	recip^#(X)	(109)
proper^#(cons(X1,X2))	→	cons^#(proper(X1),proper(X2))	(110)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(111)
top^#(mark(X))	→	top^#(proper(X))	(112)
active^#(sqr(s(X)))	→	add^#(sqr(X),dbl(X))	(113)
proper^#(half(X))	→	half^#(proper(X))	(114)
active^#(add(s(X),Y))	→	add^#(X,Y)	(115)
proper^#(terms(X))	→	terms^#(proper(X))	(116)
active^#(first(X1,X2))	→	first^#(X1,active(X2))	(117)
active^#(first(s(X),cons(Y,Z)))	→	cons^#(Y,first(X,Z))	(118)
top^#(mark(X))	→	proper^#(X)	(119)
active^#(s(X))	→	s^#(active(X))	(120)
active^#(half(X))	→	active^#(X)	(121)
active^#(sqr(X))	→	active^#(X)	(122)
proper^#(recip(X))	→	proper^#(X)	(123)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(124)
proper^#(s(X))	→	s^#(proper(X))	(125)
active^#(add(X1,X2))	→	active^#(X1)	(126)
active^#(half(X))	→	half^#(active(X))	(127)
active^#(s(X))	→	active^#(X)	(128)
active^#(dbl(X))	→	active^#(X)	(129)
active^#(terms(X))	→	active^#(X)	(130)
s^#(ok(X))	→	s^#(X)	(131)
proper^#(recip(X))	→	recip^#(proper(X))	(132)
s^#(mark(X))	→	s^#(X)	(133)
active^#(terms(N))	→	sqr^#(N)	(134)
proper^#(dbl(X))	→	dbl^#(proper(X))	(135)
sqr^#(mark(X))	→	sqr^#(X)	(136)
proper^#(add(X1,X2))	→	proper^#(X1)	(137)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(138)
half^#(mark(X))	→	half^#(X)	(139)
first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(140)
active^#(dbl(s(X)))	→	dbl^#(X)	(141)
half^#(ok(X))	→	half^#(X)	(142)

1.1 Dependency Graph Processor

The dependency pairs are split into 12 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(89)
top^#(mark(X))	→	top^#(proper(X))	(112)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	1
π(dbl^#)	=	1
π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(active)	=	1
π(cons)	=	1

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

prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(recip)	=	2	status(recip)	=	[1]	list-extension(recip)	=	Lex
prec(recip^#)	=	0	status(recip^#)	=	[]	list-extension(recip^#)	=	Lex
prec(dbl)	=	5	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(terms^#)	=	0	status(terms^#)	=	[]	list-extension(terms^#)	=	Lex
prec(half^#)	=	0	status(half^#)	=	[]	list-extension(half^#)	=	Lex
prec(half)	=	3	status(half)	=	[1]	list-extension(half)	=	Lex
prec(sqr^#)	=	0	status(sqr^#)	=	[]	list-extension(sqr^#)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(first^#)	=	0	status(first^#)	=	[]	list-extension(first^#)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(mark)	=	2	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(first)	=	4	status(first)	=	[2, 1]	list-extension(first)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(add^#)	=	0	status(add^#)	=	[1, 2]	list-extension(add^#)	=	Lex
prec(add)	=	4	status(add)	=	[1, 2]	list-extension(add)	=	Lex
prec(sqr)	=	5	status(sqr)	=	[1]	list-extension(sqr)	=	Lex
prec(terms)	=	6	status(terms)	=	[1]	list-extension(terms)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[recip(x₁)]	=	x₁ + 0
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	max(0)
[nil]	=	0
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[proper^#(x₁)]	=	0
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[sqr(x₁)]	=	x₁ + 0
[terms(x₁)]	=	x₁ + 0

together with the usable rules

active(s(X))	→	s(active(X))	(18)
sqr(ok(X))	→	ok(sqr(X))	(50)
active(dbl(0))	→	mark(0)	(4)
active(cons(X1,X2))	→	cons(active(X1),X2)	(15)
active(first(0,X))	→	mark(nil)	(8)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
active(terms(N))	→	mark(cons(recip(sqr(N)),terms(s(N))))	(1)
active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
active(recip(X))	→	recip(active(X))	(16)
active(dbl(X))	→	dbl(active(X))	(21)
proper(terms(X))	→	terms(proper(X))	(36)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(26)
active(add(X1,X2))	→	add(active(X1),X2)	(19)
dbl(mark(X))	→	mark(dbl(X))	(32)
active(sqr(X))	→	sqr(active(X))	(17)
recip(mark(X))	→	mark(recip(X))	(27)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
active(first(X1,X2))	→	first(active(X1),X2)	(22)
sqr(mark(X))	→	mark(sqr(X))	(28)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(44)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
active(half(0))	→	mark(0)	(10)
proper(sqr(X))	→	sqr(proper(X))	(39)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
active(add(X1,X2))	→	add(X1,active(X2))	(20)
terms(mark(X))	→	mark(terms(X))	(25)
recip(ok(X))	→	ok(recip(X))	(49)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
add(mark(X1),X2)	→	mark(add(X1,X2))	(30)
active(terms(X))	→	terms(active(X))	(14)
add(X1,mark(X2))	→	mark(add(X1,X2))	(31)
active(half(s(s(X))))	→	mark(s(half(X)))	(12)
proper(nil)	→	ok(nil)	(45)
active(first(X1,X2))	→	first(X1,active(X2))	(23)
active(half(X))	→	half(active(X))	(24)
active(half(s(0)))	→	mark(0)	(11)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
active(half(dbl(X)))	→	mark(X)	(13)
s(ok(X))	→	ok(s(X))	(51)
proper(s(X))	→	s(proper(X))	(40)
half(ok(X))	→	ok(half(X))	(55)
active(add(0,X))	→	mark(X)	(6)
proper(recip(X))	→	recip(proper(X))	(38)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(48)
dbl(ok(X))	→	ok(dbl(X))	(53)
terms(ok(X))	→	ok(terms(X))	(47)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(37)
proper(0)	→	ok(0)	(41)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(42)
proper(half(X))	→	half(proper(X))	(46)
half(mark(X))	→	mark(half(X))	(35)
s(mark(X))	→	mark(s(X))	(29)
proper(dbl(X))	→	dbl(proper(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(112)

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))

(89)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[recip(x₁)]	=	x₁ + 0
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	28473
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	28471
[mark(x₁)]	=	0
[first(x₁, x₂)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 0
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 0
[sqr(x₁)]	=	x₁ + 0
[terms(x₁)]	=	x₁ + 0

together with the usable rules

active(s(X))	→	s(active(X))	(18)
sqr(ok(X))	→	ok(sqr(X))	(50)
active(dbl(0))	→	mark(0)	(4)
active(cons(X1,X2))	→	cons(active(X1),X2)	(15)
active(first(0,X))	→	mark(nil)	(8)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
active(terms(N))	→	mark(cons(recip(sqr(N)),terms(s(N))))	(1)
active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
active(recip(X))	→	recip(active(X))	(16)
active(dbl(X))	→	dbl(active(X))	(21)
proper(terms(X))	→	terms(proper(X))	(36)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(26)
active(add(X1,X2))	→	add(active(X1),X2)	(19)
dbl(mark(X))	→	mark(dbl(X))	(32)
active(sqr(X))	→	sqr(active(X))	(17)
recip(mark(X))	→	mark(recip(X))	(27)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
active(first(X1,X2))	→	first(active(X1),X2)	(22)
sqr(mark(X))	→	mark(sqr(X))	(28)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(44)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
active(half(0))	→	mark(0)	(10)
proper(sqr(X))	→	sqr(proper(X))	(39)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
active(add(X1,X2))	→	add(X1,active(X2))	(20)
terms(mark(X))	→	mark(terms(X))	(25)
recip(ok(X))	→	ok(recip(X))	(49)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
add(mark(X1),X2)	→	mark(add(X1,X2))	(30)
active(terms(X))	→	terms(active(X))	(14)
add(X1,mark(X2))	→	mark(add(X1,X2))	(31)
active(half(s(s(X))))	→	mark(s(half(X)))	(12)
proper(nil)	→	ok(nil)	(45)
active(first(X1,X2))	→	first(X1,active(X2))	(23)
active(half(X))	→	half(active(X))	(24)
active(half(s(0)))	→	mark(0)	(11)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
active(half(dbl(X)))	→	mark(X)	(13)
s(ok(X))	→	ok(s(X))	(51)
proper(s(X))	→	s(proper(X))	(40)
half(ok(X))	→	ok(half(X))	(55)
active(add(0,X))	→	mark(X)	(6)
proper(recip(X))	→	recip(proper(X))	(38)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(48)
dbl(ok(X))	→	ok(dbl(X))	(53)
terms(ok(X))	→	ok(terms(X))	(47)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(37)
proper(0)	→	ok(0)	(41)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(42)
proper(half(X))	→	half(proper(X))	(46)
half(mark(X))	→	mark(half(X))	(35)
s(mark(X))	→	mark(s(X))	(29)
proper(dbl(X))	→	dbl(proper(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

top^#(ok(X))

→

top^#(active(X))

(89)

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^#(cons(X1,X2))	→	active^#(X1)	(100)
active^#(first(X1,X2))	→	active^#(X1)	(99)
active^#(recip(X))	→	active^#(X)	(90)
active^#(terms(X))	→	active^#(X)	(130)
active^#(dbl(X))	→	active^#(X)	(129)
active^#(s(X))	→	active^#(X)	(128)
active^#(add(X1,X2))	→	active^#(X1)	(126)
active^#(sqr(X))	→	active^#(X)	(122)
active^#(half(X))	→	active^#(X)	(121)
active^#(add(X1,X2))	→	active^#(X2)	(65)
active^#(first(X1,X2))	→	active^#(X2)	(60)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[recip(x₁)]	=	x₁ + 0
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 2
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	x₁ + x₂ + 0
[proper^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 0
[sqr(x₁)]	=	x₁ + 0
[terms(x₁)]	=	x₁ + 1

together with the usable rules

active(dbl(0))	→	mark(0)	(4)
active(first(0,X))	→	mark(nil)	(8)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
dbl(mark(X))	→	mark(dbl(X))	(32)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
active(half(0))	→	mark(0)	(10)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
add(mark(X1),X2)	→	mark(add(X1,X2))	(30)
add(X1,mark(X2))	→	mark(add(X1,X2))	(31)
active(half(s(0)))	→	mark(0)	(11)
active(half(dbl(X)))	→	mark(X)	(13)
active(add(0,X))	→	mark(X)	(6)
dbl(ok(X))	→	ok(dbl(X))	(53)
active(sqr(0))	→	mark(0)	(2)

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

active^#(terms(X))

→

active^#(X)

(130)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(s(X))	→	active^#(X)	(128)
active^#(cons(X1,X2))	→	active^#(X1)	(100)
active^#(recip(X))	→	active^#(X)	(90)
active^#(dbl(X))	→	active^#(X)	(129)
active^#(add(X1,X2))	→	active^#(X1)	(126)
active^#(sqr(X))	→	active^#(X)	(122)
active^#(first(X1,X2))	→	active^#(X1)	(99)
active^#(add(X1,X2))	→	active^#(X2)	(65)
active^#(first(X1,X2))	→	active^#(X2)	(60)
active^#(half(X))	→	active^#(X)	(121)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[recip(x₁)]	=	x₁ + 1
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 24817
[ok(x₁)]	=	x₁ + 24818
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	0
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[sqr(x₁)]	=	x₁ + 1
[terms(x₁)]	=	x₁ + 1

together with the usable rules

active(dbl(0))	→	mark(0)	(4)
active(first(0,X))	→	mark(nil)	(8)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
dbl(mark(X))	→	mark(dbl(X))	(32)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
active(half(0))	→	mark(0)	(10)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
add(mark(X1),X2)	→	mark(add(X1,X2))	(30)
add(X1,mark(X2))	→	mark(add(X1,X2))	(31)
active(half(s(0)))	→	mark(0)	(11)
active(half(dbl(X)))	→	mark(X)	(13)
active(add(0,X))	→	mark(X)	(6)
dbl(ok(X))	→	ok(dbl(X))	(53)
active(sqr(0))	→	mark(0)	(2)

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

active^#(cons(X1,X2))	→	active^#(X1)	(100)
active^#(recip(X))	→	active^#(X)	(90)
active^#(dbl(X))	→	active^#(X)	(129)
active^#(add(X1,X2))	→	active^#(X1)	(126)
active^#(sqr(X))	→	active^#(X)	(122)
active^#(first(X1,X2))	→	active^#(X1)	(99)
active^#(add(X1,X2))	→	active^#(X2)	(65)
active^#(first(X1,X2))	→	active^#(X2)	(60)
active^#(half(X))	→	active^#(X)	(121)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(s(X))

→

active^#(X)

(128)

1.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[recip(x₁)]	=	x₁ + 1
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 6620
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	9129
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	3
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 4
[proper^#(x₁)]	=	0
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 10288
[sqr(x₁)]	=	x₁ + 1
[terms(x₁)]	=	x₁ + 1

together with the usable rules

active(dbl(0))	→	mark(0)	(4)
active(first(0,X))	→	mark(nil)	(8)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
active(half(0))	→	mark(0)	(10)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
active(half(s(0)))	→	mark(0)	(11)
dbl(ok(X))	→	ok(dbl(X))	(53)
active(sqr(0))	→	mark(0)	(2)

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

active^#(s(X))

→

active^#(X)

(128)

could be deleted.

1.1.2.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

proper^#(first(X1,X2))	→	proper^#(X1)	(104)
proper^#(cons(X1,X2))	→	proper^#(X2)	(96)
proper^#(add(X1,X2))	→	proper^#(X1)	(137)
proper^#(cons(X1,X2))	→	proper^#(X1)	(86)
proper^#(add(X1,X2))	→	proper^#(X2)	(85)
proper^#(recip(X))	→	proper^#(X)	(123)
proper^#(half(X))	→	proper^#(X)	(78)
proper^#(first(X1,X2))	→	proper^#(X2)	(70)
proper^#(sqr(X))	→	proper^#(X)	(64)
proper^#(terms(X))	→	proper^#(X)	(63)
proper^#(dbl(X))	→	proper^#(X)	(58)
proper^#(s(X))	→	proper^#(X)	(107)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[recip(x₁)]	=	x₁ + 13745
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 13457
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 9123
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	3
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	15795
[first(x₁, x₂)]	=	x₁ + x₂ + 22746
[proper^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	17406
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 6860
[sqr(x₁)]	=	x₁ + 1
[terms(x₁)]	=	x₁ + 1

together with the usable rules

active(dbl(0))	→	mark(0)	(4)
active(first(0,X))	→	mark(nil)	(8)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)
active(half(0))	→	mark(0)	(10)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(52)
add(X1,mark(X2))	→	mark(add(X1,X2))	(31)
active(half(s(0)))	→	mark(0)	(11)
dbl(ok(X))	→	ok(dbl(X))	(53)
active(sqr(0))	→	mark(0)	(2)

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

proper^#(first(X1,X2))	→	proper^#(X1)	(104)
proper^#(cons(X1,X2))	→	proper^#(X2)	(96)
proper^#(add(X1,X2))	→	proper^#(X1)	(137)
proper^#(cons(X1,X2))	→	proper^#(X1)	(86)
proper^#(add(X1,X2))	→	proper^#(X2)	(85)
proper^#(recip(X))	→	proper^#(X)	(123)
proper^#(half(X))	→	proper^#(X)	(78)
proper^#(first(X1,X2))	→	proper^#(X2)	(70)
proper^#(sqr(X))	→	proper^#(X)	(64)
proper^#(terms(X))	→	proper^#(X)	(63)
proper^#(dbl(X))	→	proper^#(X)	(58)
proper^#(s(X))	→	proper^#(X)	(107)

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

dbl^#(ok(X))	→	dbl^#(X)	(101)
dbl^#(mark(X))	→	dbl^#(X)	(76)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 9589
[recip(x₁)]	=	28967
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 49976
[top(x₁)]	=	0
[dbl^#(x₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 51752
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 21639
[0]	=	30728
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 28117
[first(x₁, x₂)]	=	x₁ + x₂ + 8127
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	x₁ + x₂ + 29518
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 27234
[sqr(x₁)]	=	26325
[terms(x₁)]	=	26534

together with the usable rules

first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(54)
first(X1,mark(X2))	→	mark(first(X1,X2))	(34)
first(mark(X1),X2)	→	mark(first(X1,X2))	(33)

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

dbl^#(ok(X))	→	dbl^#(X)	(101)
dbl^#(mark(X))	→	dbl^#(X)	(76)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

half^#(ok(X))	→	half^#(X)	(142)
half^#(mark(X))	→	half^#(X)	(139)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	8137
[recip(x₁)]	=	1428
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	2
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	x₁ + 0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 2874
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	23191
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	25338
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	x₂ + 22612
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 7803
[sqr(x₁)]	=	x₁ + 21331
[terms(x₁)]	=	37936

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

half^#(ok(X))	→	half^#(X)	(142)
half^#(mark(X))	→	half^#(X)	(139)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

add^#(X1,mark(X2))	→	add^#(X1,X2)	(124)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(77)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(67)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	33286
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	12341
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	47761
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	16689
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	31853
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	7803
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(77)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(67)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

add^#(X1,mark(X2))

→

add^#(X1,X2)

(124)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	33286
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	12341
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	26389
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	2
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₂ + 0
[add(x₁, x₂)]	=	2
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

add^#(X1,mark(X2))

→

add^#(X1,X2)

(124)

could be deleted.

1.1.6.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(138)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(111)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	42037
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	12341
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	5609
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	21952
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	4686
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	26405
[sqr(x₁)]	=	12115
[terms(x₁)]	=	3343

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

cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(138)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(111)

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

recip^#(mark(X))	→	recip^#(X)	(75)
recip^#(ok(X))	→	recip^#(X)	(109)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	73860
[recip(x₁)]	=	2
[recip^#(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	12341
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 4000
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1610
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	21952
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	19315
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	26405
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

recip^#(mark(X))	→	recip^#(X)	(75)
recip^#(ok(X))	→	recip^#(X)	(109)

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

s^#(mark(X))	→	s^#(X)	(133)
s^#(ok(X))	→	s^#(X)	(131)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	89514
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	12341
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 408
[0]	=	1
[s^#(x₁)]	=	x₁ + 0
[first^#(x₁, x₂)]	=	0
[nil]	=	1203
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	21952
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	13069
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	23102
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

s^#(mark(X))	→	s^#(X)	(133)
s^#(ok(X))	→	s^#(X)	(131)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

sqr^#(mark(X))	→	sqr^#(X)	(136)
sqr^#(ok(X))	→	sqr^#(X)	(62)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	117474
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	12341
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	9481
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	21952
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	31595
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	12761
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

sqr^#(mark(X))	→	sqr^#(X)	(136)
sqr^#(ok(X))	→	sqr^#(X)	(62)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(140)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(87)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(69)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	121223
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	2
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	x₁ + 0
[nil]	=	1
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	31104
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	14862
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	12064
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(140)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(69)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

first^#(X1,mark(X2))

→

first^#(X1,X2)

(87)

1.1.11.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	145449
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	2
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	x₂ + 0
[nil]	=	56833
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	29829
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	15093
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	2
[sqr(x₁)]	=	12115
[terms(x₁)]	=	2

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

first^#(X1,mark(X2))

→

first^#(X1,X2)

(87)

could be deleted.

1.1.11.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 12^th component contains the pair

terms^#(ok(X))	→	terms^#(X)	(84)
terms^#(mark(X))	→	terms^#(X)	(82)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	154603
[recip(x₁)]	=	2
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	29899
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	2201
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 2
[first(x₁, x₂)]	=	4037
[proper^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	26835
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	31781
[sqr(x₁)]	=	12115
[terms(x₁)]	=	20846

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

terms^#(ok(X))	→	terms^#(X)	(84)
terms^#(mark(X))	→	terms^#(X)	(82)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 0 components.