Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex2_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(terms(X))	→	terms(active(X))	(10)
active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
active(recip(X))	→	recip(active(X))	(12)
active(sqr(X))	→	sqr(active(X))	(13)
active(s(X))	→	s(active(X))	(14)
active(add(X1,X2))	→	add(active(X1),X2)	(15)
active(add(X1,X2))	→	add(X1,active(X2))	(16)
active(dbl(X))	→	dbl(active(X))	(17)
active(first(X1,X2))	→	first(active(X1),X2)	(18)
active(first(X1,X2))	→	first(X1,active(X2))	(19)
terms(mark(X))	→	mark(terms(X))	(20)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
recip(mark(X))	→	mark(recip(X))	(22)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
add(mark(X1),X2)	→	mark(add(X1,X2))	(25)
add(X1,mark(X2))	→	mark(add(X1,X2))	(26)
dbl(mark(X))	→	mark(dbl(X))	(27)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
proper(terms(X))	→	terms(proper(X))	(30)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(31)
proper(recip(X))	→	recip(proper(X))	(32)
proper(sqr(X))	→	sqr(proper(X))	(33)
proper(s(X))	→	s(proper(X))	(34)
proper(0)	→	ok(0)	(35)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(36)
proper(dbl(X))	→	dbl(proper(X))	(37)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(38)
proper(nil)	→	ok(nil)	(39)
terms(ok(X))	→	ok(terms(X))	(40)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
sqr(ok(X))	→	ok(sqr(X))	(43)
s(ok(X))	→	ok(s(X))	(44)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(45)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
top(mark(X))	→	top(proper(X))	(48)
top(ok(X))	→	top(active(X))	(49)

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.

first^#(X1,mark(X2))	→	first^#(X1,X2)	(50)
active^#(dbl(s(X)))	→	s^#(s(dbl(X)))	(51)
active^#(s(X))	→	s^#(active(X))	(52)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(53)
active^#(sqr(s(X)))	→	add^#(sqr(X),dbl(X))	(54)
s^#(ok(X))	→	s^#(X)	(55)
proper^#(sqr(X))	→	proper^#(X)	(56)
proper^#(sqr(X))	→	sqr^#(proper(X))	(57)
active^#(add(s(X),Y))	→	s^#(add(X,Y))	(58)
active^#(terms(N))	→	s^#(N)	(59)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(60)
active^#(dbl(X))	→	active^#(X)	(61)
active^#(terms(N))	→	sqr^#(N)	(62)
recip^#(mark(X))	→	recip^#(X)	(63)
active^#(add(X1,X2))	→	active^#(X1)	(64)
active^#(add(X1,X2))	→	add^#(active(X1),X2)	(65)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(66)
proper^#(add(X1,X2))	→	proper^#(X2)	(67)
active^#(add(s(X),Y))	→	add^#(X,Y)	(68)
proper^#(dbl(X))	→	dbl^#(proper(X))	(69)
proper^#(add(X1,X2))	→	add^#(proper(X1),proper(X2))	(70)
proper^#(recip(X))	→	proper^#(X)	(71)
active^#(sqr(s(X)))	→	sqr^#(X)	(72)
active^#(terms(X))	→	active^#(X)	(73)
dbl^#(mark(X))	→	dbl^#(X)	(74)
proper^#(first(X1,X2))	→	proper^#(X2)	(75)
top^#(mark(X))	→	top^#(proper(X))	(76)
proper^#(first(X1,X2))	→	first^#(proper(X1),proper(X2))	(77)
active^#(first(X1,X2))	→	active^#(X2)	(78)
active^#(first(X1,X2))	→	first^#(active(X1),X2)	(79)
active^#(recip(X))	→	recip^#(active(X))	(80)
active^#(terms(N))	→	recip^#(sqr(N))	(81)
add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(82)
active^#(dbl(s(X)))	→	dbl^#(X)	(83)
active^#(terms(N))	→	cons^#(recip(sqr(N)),terms(s(N)))	(84)
proper^#(first(X1,X2))	→	proper^#(X1)	(85)
proper^#(terms(X))	→	terms^#(proper(X))	(86)
active^#(first(X1,X2))	→	first^#(X1,active(X2))	(87)
terms^#(ok(X))	→	terms^#(X)	(88)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(89)
active^#(s(X))	→	active^#(X)	(90)
active^#(dbl(X))	→	dbl^#(active(X))	(91)
proper^#(s(X))	→	s^#(proper(X))	(92)
active^#(recip(X))	→	active^#(X)	(93)
active^#(cons(X1,X2))	→	active^#(X1)	(94)
proper^#(dbl(X))	→	proper^#(X)	(95)
active^#(terms(X))	→	terms^#(active(X))	(96)
top^#(mark(X))	→	proper^#(X)	(97)
active^#(add(X1,X2))	→	active^#(X2)	(98)
top^#(ok(X))	→	top^#(active(X))	(99)
active^#(terms(N))	→	terms^#(s(N))	(100)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(101)
active^#(dbl(s(X)))	→	s^#(dbl(X))	(102)
active^#(sqr(s(X)))	→	s^#(add(sqr(X),dbl(X)))	(103)
proper^#(cons(X1,X2))	→	proper^#(X2)	(104)
sqr^#(mark(X))	→	sqr^#(X)	(105)
top^#(ok(X))	→	active^#(X)	(106)
proper^#(cons(X1,X2))	→	proper^#(X1)	(107)
proper^#(add(X1,X2))	→	proper^#(X1)	(108)
active^#(first(s(X),cons(Y,Z)))	→	cons^#(Y,first(X,Z))	(109)
proper^#(terms(X))	→	proper^#(X)	(110)
active^#(cons(X1,X2))	→	cons^#(active(X1),X2)	(111)
active^#(add(X1,X2))	→	add^#(X1,active(X2))	(112)
proper^#(cons(X1,X2))	→	cons^#(proper(X1),proper(X2))	(113)
active^#(sqr(s(X)))	→	dbl^#(X)	(114)
terms^#(mark(X))	→	terms^#(X)	(115)
s^#(mark(X))	→	s^#(X)	(116)
active^#(sqr(X))	→	active^#(X)	(117)
dbl^#(ok(X))	→	dbl^#(X)	(118)
active^#(first(X1,X2))	→	active^#(X1)	(119)
sqr^#(ok(X))	→	sqr^#(X)	(120)
proper^#(recip(X))	→	recip^#(proper(X))	(121)
first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(122)
active^#(sqr(X))	→	sqr^#(active(X))	(123)
recip^#(ok(X))	→	recip^#(X)	(124)
proper^#(s(X))	→	proper^#(X)	(125)
active^#(first(s(X),cons(Y,Z)))	→	first^#(X,Z)	(126)

1.1 Dependency Graph Processor

The dependency pairs are split into 11 components.

The 1^st component contains the pair

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	2
π(recip)	=	1
π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(s^#)	=	1
π(active)	=	1
π(cons)	=	1

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

prec(s)	=	2	status(s)	=	[1]	list-extension(s)	=	Lex
prec(recip^#)	=	0	status(recip^#)	=	[]	list-extension(recip^#)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(terms^#)	=	0	status(terms^#)	=	[]	list-extension(terms^#)	=	Lex
prec(sqr^#)	=	0	status(sqr^#)	=	[]	list-extension(sqr^#)	=	Lex
prec(0)	=	5	status(0)	=	[]	list-extension(0)	=	Lex
prec(first^#)	=	0	status(first^#)	=	[1, 2]	list-extension(first^#)	=	Lex
prec(nil)	=	1	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(mark)	=	2	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(first)	=	6	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^#)	=	[]	list-extension(add^#)	=	Lex
prec(add)	=	3	status(add)	=	[2, 1]	list-extension(add)	=	Lex
prec(sqr)	=	4	status(sqr)	=	[1]	list-extension(sqr)	=	Lex
prec(terms)	=	5	status(terms)	=	[1]	list-extension(terms)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[first^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 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(0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[sqr(x₁)]	=	x₁ + 0
[terms(x₁)]	=	x₁ + 0

together with the usable rules

active(first(X1,X2))	→	first(active(X1),X2)	(18)
active(dbl(0))	→	mark(0)	(4)
active(add(X1,X2))	→	add(active(X1),X2)	(15)
active(first(0,X))	→	mark(nil)	(8)
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(add(X1,X2))	→	add(X1,active(X2))	(16)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(36)
add(X1,mark(X2))	→	mark(add(X1,X2))	(26)
active(first(X1,X2))	→	first(X1,active(X2))	(19)
proper(recip(X))	→	recip(proper(X))	(32)
active(dbl(X))	→	dbl(active(X))	(17)
dbl(mark(X))	→	mark(dbl(X))	(27)
proper(s(X))	→	s(proper(X))	(34)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
proper(sqr(X))	→	sqr(proper(X))	(33)
active(terms(X))	→	terms(active(X))	(10)
proper(nil)	→	ok(nil)	(39)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
terms(mark(X))	→	mark(terms(X))	(20)
add(mark(X1),X2)	→	mark(add(X1,X2))	(25)
proper(terms(X))	→	terms(proper(X))	(30)
active(s(X))	→	s(active(X))	(14)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(31)
active(recip(X))	→	recip(active(X))	(12)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(45)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
active(sqr(X))	→	sqr(active(X))	(13)
terms(ok(X))	→	ok(terms(X))	(40)
active(add(0,X))	→	mark(X)	(6)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(38)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
proper(dbl(X))	→	dbl(proper(X))	(37)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
proper(0)	→	ok(0)	(35)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(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))

(76)

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

(99)

1.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₁ + 9245
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 13826
[ok(x₁)]	=	x₁ + 13826
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	43318
[mark(x₁)]	=	0
[first(x₁, x₂)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 57534
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 0
[sqr(x₁)]	=	x₁ + 1
[terms(x₁)]	=	x₁ + 1

together with the usable rules

active(first(X1,X2))	→	first(active(X1),X2)	(18)
active(dbl(0))	→	mark(0)	(4)
active(add(X1,X2))	→	add(active(X1),X2)	(15)
active(first(0,X))	→	mark(nil)	(8)
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(add(X1,X2))	→	add(X1,active(X2))	(16)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(36)
add(X1,mark(X2))	→	mark(add(X1,X2))	(26)
active(first(X1,X2))	→	first(X1,active(X2))	(19)
proper(recip(X))	→	recip(proper(X))	(32)
active(dbl(X))	→	dbl(active(X))	(17)
dbl(mark(X))	→	mark(dbl(X))	(27)
proper(s(X))	→	s(proper(X))	(34)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
proper(sqr(X))	→	sqr(proper(X))	(33)
active(terms(X))	→	terms(active(X))	(10)
proper(nil)	→	ok(nil)	(39)
active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
terms(mark(X))	→	mark(terms(X))	(20)
add(mark(X1),X2)	→	mark(add(X1,X2))	(25)
proper(terms(X))	→	terms(proper(X))	(30)
active(s(X))	→	s(active(X))	(14)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(31)
active(recip(X))	→	recip(active(X))	(12)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(45)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
active(sqr(X))	→	sqr(active(X))	(13)
terms(ok(X))	→	ok(terms(X))	(40)
active(add(0,X))	→	mark(X)	(6)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(38)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
proper(dbl(X))	→	dbl(proper(X))	(37)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
proper(0)	→	ok(0)	(35)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(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))

(99)

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

proper^#(s(X))	→	proper^#(X)	(125)
proper^#(first(X1,X2))	→	proper^#(X1)	(85)
proper^#(first(X1,X2))	→	proper^#(X2)	(75)
proper^#(terms(X))	→	proper^#(X)	(110)
proper^#(recip(X))	→	proper^#(X)	(71)
proper^#(add(X1,X2))	→	proper^#(X1)	(108)
proper^#(cons(X1,X2))	→	proper^#(X1)	(107)
proper^#(add(X1,X2))	→	proper^#(X2)	(67)
proper^#(cons(X1,X2))	→	proper^#(X2)	(104)
proper^#(sqr(X))	→	proper^#(X)	(56)
proper^#(dbl(X))	→	proper^#(X)	(95)

1.1.2 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₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	3965
[0]	=	13826
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	12927
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	13826
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(36)
add(X1,mark(X2))	→	mark(add(X1,X2))	(26)
proper(recip(X))	→	recip(proper(X))	(32)
dbl(mark(X))	→	mark(dbl(X))	(27)
proper(s(X))	→	s(proper(X))	(34)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
proper(sqr(X))	→	sqr(proper(X))	(33)
proper(nil)	→	ok(nil)	(39)
terms(mark(X))	→	mark(terms(X))	(20)
add(mark(X1),X2)	→	mark(add(X1,X2))	(25)
proper(terms(X))	→	terms(proper(X))	(30)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(31)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(45)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(38)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
proper(dbl(X))	→	dbl(proper(X))	(37)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
proper(0)	→	ok(0)	(35)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

proper^#(s(X))	→	proper^#(X)	(125)
proper^#(first(X1,X2))	→	proper^#(X1)	(85)
proper^#(first(X1,X2))	→	proper^#(X2)	(75)
proper^#(terms(X))	→	proper^#(X)	(110)
proper^#(recip(X))	→	proper^#(X)	(71)
proper^#(add(X1,X2))	→	proper^#(X1)	(108)
proper^#(cons(X1,X2))	→	proper^#(X1)	(107)
proper^#(add(X1,X2))	→	proper^#(X2)	(67)
proper^#(cons(X1,X2))	→	proper^#(X2)	(104)
proper^#(sqr(X))	→	proper^#(X)	(56)
proper^#(dbl(X))	→	proper^#(X)	(95)

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

active^#(recip(X))	→	active^#(X)	(93)
active^#(s(X))	→	active^#(X)	(90)
active^#(first(X1,X2))	→	active^#(X1)	(119)
active^#(sqr(X))	→	active^#(X)	(117)
active^#(first(X1,X2))	→	active^#(X2)	(78)
active^#(terms(X))	→	active^#(X)	(73)
active^#(add(X1,X2))	→	active^#(X1)	(64)
active^#(dbl(X))	→	active^#(X)	(61)
active^#(add(X1,X2))	→	active^#(X2)	(98)
active^#(cons(X1,X2))	→	active^#(X1)	(94)

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₁ + 1
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	1
[0]	=	13826
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	12927
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	13826
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(36)
add(X1,mark(X2))	→	mark(add(X1,X2))	(26)
proper(recip(X))	→	recip(proper(X))	(32)
dbl(mark(X))	→	mark(dbl(X))	(27)
proper(s(X))	→	s(proper(X))	(34)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
proper(sqr(X))	→	sqr(proper(X))	(33)
proper(nil)	→	ok(nil)	(39)
terms(mark(X))	→	mark(terms(X))	(20)
add(mark(X1),X2)	→	mark(add(X1,X2))	(25)
proper(terms(X))	→	terms(proper(X))	(30)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(31)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(45)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(38)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
proper(dbl(X))	→	dbl(proper(X))	(37)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
proper(0)	→	ok(0)	(35)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

active^#(recip(X))	→	active^#(X)	(93)
active^#(s(X))	→	active^#(X)	(90)
active^#(first(X1,X2))	→	active^#(X1)	(119)
active^#(sqr(X))	→	active^#(X)	(117)
active^#(first(X1,X2))	→	active^#(X2)	(78)
active^#(terms(X))	→	active^#(X)	(73)
active^#(add(X1,X2))	→	active^#(X1)	(64)
active^#(dbl(X))	→	active^#(X)	(61)
active^#(add(X1,X2))	→	active^#(X2)	(98)
active^#(cons(X1,X2))	→	active^#(X1)	(94)

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)	(118)
dbl^#(mark(X))	→	dbl^#(X)	(74)

1.1.4 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₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	5
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + x₂ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
add(X1,mark(X2))	→	mark(add(X1,X2))	(26)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
add(mark(X1),X2)	→	mark(add(X1,X2))	(25)
add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(45)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

dbl^#(ok(X))

→

dbl^#(X)

(118)

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

dbl^#(mark(X))

→

dbl^#(X)

(74)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 14756
[recip(x₁)]	=	x₁ + 8855
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 23613
[proper^#(x₁)]	=	0
[active(x₁)]	=	51949
[cons(x₁, x₂)]	=	x₁ + x₂ + 28335
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

dbl^#(mark(X))

→

dbl^#(X)

(74)

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(89)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(101)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 1
[recip(x₁)]	=	x₁ + 1
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	8
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

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

→

cons^#(X1,X2)

(101)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(89)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[recip(x₁)]	=	x₁ + 1
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 4
[proper^#(x₁)]	=	0
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(89)

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

recip^#(ok(X))	→	recip^#(X)	(124)
recip^#(mark(X))	→	recip^#(X)	(63)

1.1.6 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₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 4
[proper^#(x₁)]	=	0
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

recip^#(ok(X))	→	recip^#(X)	(124)
recip^#(mark(X))	→	recip^#(X)	(63)

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

sqr^#(ok(X))	→	sqr^#(X)	(120)
sqr^#(mark(X))	→	sqr^#(X)	(105)

1.1.7 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₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	17214
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[sqr(x₁)]	=	x₁ + 1
[terms(x₁)]	=	x₁ + 17209

together with the usable rules

active(dbl(0))	→	mark(0)	(4)
active(first(0,X))	→	mark(nil)	(8)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

sqr^#(ok(X))	→	sqr^#(X)	(120)
sqr^#(mark(X))	→	sqr^#(X)	(105)

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

terms^#(ok(X))	→	terms^#(X)	(88)
terms^#(mark(X))	→	terms^#(X)	(115)

1.1.8 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₁ + 3
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 4
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 4
[proper^#(x₁)]	=	0
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

terms^#(ok(X))	→	terms^#(X)	(88)
terms^#(mark(X))	→	terms^#(X)	(115)

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)	(116)
s^#(ok(X))	→	s^#(X)	(55)

1.1.9 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₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	x₁ + 0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

s^#(mark(X))	→	s^#(X)	(116)
s^#(ok(X))	→	s^#(X)	(55)

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

add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(82)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(66)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(53)

1.1.10 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₁ + 1
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[first(x₁, x₂)]	=	x₁ + x₂ + 4
[proper^#(x₁)]	=	0
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	x₁ + 0
[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)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
dbl(mark(X))	→	mark(dbl(X))	(27)
recip(mark(X))	→	mark(recip(X))	(22)
first(mark(X1),X2)	→	mark(first(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(44)
terms(mark(X))	→	mark(terms(X))	(20)
sqr(mark(X))	→	mark(sqr(X))	(23)
s(mark(X))	→	mark(s(X))	(24)
terms(ok(X))	→	ok(terms(X))	(40)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
dbl(ok(X))	→	ok(dbl(X))	(46)
first(X1,mark(X2))	→	mark(first(X1,X2))	(29)
sqr(ok(X))	→	ok(sqr(X))	(43)
active(sqr(0))	→	mark(0)	(2)

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

add^#(ok(X1),ok(X2))	→	add^#(X1,X2)	(82)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(53)

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

add^#(X1,mark(X2))

→

add^#(X1,X2)

(66)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[recip(x₁)]	=	x₁ + 23802
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 2154
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1233
[0]	=	1870
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	22003
[mark(x₁)]	=	x₁ + 16777
[first(x₁, x₂)]	=	x₂ + 1
[proper^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 14622
[cons(x₁, x₂)]	=	x₂ + 11204
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₂ + 0
[add(x₁, x₂)]	=	x₂ + 221
[sqr(x₁)]	=	1788
[terms(x₁)]	=	x₁ + 18871

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

add^#(X1,mark(X2))

→

add^#(X1,X2)

(66)

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

first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(122)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(60)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(50)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 23622
[recip(x₁)]	=	x₁ + 57912
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 29828
[top(x₁)]	=	0
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[top^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	11969
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	32156
[mark(x₁)]	=	x₁ + 60159
[first(x₁, x₂)]	=	1
[proper^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 16121
[cons(x₁, x₂)]	=	x₁ + x₂ + 48860
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 44037
[sqr(x₁)]	=	x₁ + 1
[terms(x₁)]	=	x₁ + 38224

together with the usable rules

cons(mark(X1),X2)	→	mark(cons(X1,X2))	(21)
recip(mark(X))	→	mark(recip(X))	(22)
sqr(mark(X))	→	mark(sqr(X))	(23)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(41)
recip(ok(X))	→	ok(recip(X))	(42)
sqr(ok(X))	→	ok(sqr(X))	(43)

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

first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(122)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(60)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(50)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 0 components.