Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_Luc02a_iGM)

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

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

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(132)
mark^#(first(X1,X2))	→	mark^#(X2)	(96)
mark^#(first(X1,X2))	→	active^#(first(mark(X1),mark(X2)))	(97)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(94)
mark^#(terms(X))	→	mark^#(X)	(95)
active^#(half(dbl(X)))	→	mark^#(X)	(93)
mark^#(cons(X1,X2))	→	mark^#(X1)	(92)
active^#(first(s(X),cons(Y,Z)))	→	mark^#(cons(Y,first(X,Z)))	(130)
active^#(add(0,X))	→	mark^#(X)	(88)
active^#(half(s(s(X))))	→	mark^#(s(half(X)))	(81)
mark^#(half(X))	→	mark^#(X)	(123)
mark^#(add(X1,X2))	→	mark^#(X2)	(122)
mark^#(sqr(X))	→	mark^#(X)	(79)
active^#(sqr(s(X)))	→	mark^#(s(add(sqr(X),dbl(X))))	(121)
mark^#(first(X1,X2))	→	mark^#(X1)	(75)
mark^#(half(X))	→	active^#(half(mark(X)))	(117)
mark^#(recip(X))	→	mark^#(X)	(73)
mark^#(sqr(X))	→	active^#(sqr(mark(X)))	(72)
mark^#(s(X))	→	active^#(s(mark(X)))	(112)
mark^#(terms(X))	→	active^#(terms(mark(X)))	(109)
mark^#(recip(X))	→	active^#(recip(mark(X)))	(108)
active^#(terms(N))	→	mark^#(cons(recip(sqr(N)),terms(s(N))))	(60)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(59)
mark^#(dbl(X))	→	mark^#(X)	(103)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(104)
mark^#(add(X1,X2))	→	mark^#(X1)	(53)
mark^#(s(X))	→	mark^#(X)	(50)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(51)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	9711
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	10452
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	10452
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	10452
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[first(x₁, x₂)]	=	10452
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	10451
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	10452
[sqr(x₁)]	=	10452
[terms(x₁)]	=	10452

together with the usable rules

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

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

mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(132)
mark^#(s(X))	→	active^#(s(mark(X)))	(112)
mark^#(recip(X))	→	active^#(recip(mark(X)))	(108)

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

mark^#(s(X))	→	mark^#(X)	(50)
mark^#(cons(X1,X2))	→	mark^#(X1)	(92)
active^#(terms(N))	→	mark^#(cons(recip(sqr(N)),terms(s(N))))	(60)
active^#(sqr(s(X)))	→	mark^#(s(add(sqr(X),dbl(X))))	(121)
mark^#(recip(X))	→	mark^#(X)	(73)
mark^#(dbl(X))	→	mark^#(X)	(103)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(94)
mark^#(sqr(X))	→	mark^#(X)	(79)
mark^#(sqr(X))	→	active^#(sqr(mark(X)))	(72)
mark^#(first(X1,X2))	→	mark^#(X2)	(96)
mark^#(first(X1,X2))	→	mark^#(X1)	(75)
mark^#(first(X1,X2))	→	active^#(first(mark(X1),mark(X2)))	(97)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(51)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(59)
mark^#(add(X1,X2))	→	mark^#(X2)	(122)
mark^#(add(X1,X2))	→	mark^#(X1)	(53)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(104)
mark^#(terms(X))	→	mark^#(X)	(95)
mark^#(terms(X))	→	active^#(terms(mark(X)))	(109)
active^#(half(s(s(X))))	→	mark^#(s(half(X)))	(81)
mark^#(half(X))	→	mark^#(X)	(123)
mark^#(half(X))	→	active^#(half(mark(X)))	(117)
active^#(first(s(X),cons(Y,Z)))	→	mark^#(cons(Y,first(X,Z)))	(130)
active^#(half(dbl(X)))	→	mark^#(X)	(93)
active^#(add(0,X))	→	mark^#(X)	(88)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[recip(x₁)]	=	x₁ + 28101
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 11798
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 8366
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	33428
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	max(0)
[nil]	=	30614
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	max(x₁ + 41064, x₂ + 30613, 0)
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 41065, 0)
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	max(0)
[add(x₁, x₂)]	=	max(x₁ + 0, x₂ + 5854, 0)
[sqr(x₁)]	=	x₁ + 17653
[terms(x₁)]	=	x₁ + 86820

together with the usable rules

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

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

mark^#(cons(X1,X2))	→	mark^#(X1)	(92)
active^#(terms(N))	→	mark^#(cons(recip(sqr(N)),terms(s(N))))	(60)
mark^#(recip(X))	→	mark^#(X)	(73)
mark^#(dbl(X))	→	mark^#(X)	(103)
mark^#(sqr(X))	→	mark^#(X)	(79)
mark^#(first(X1,X2))	→	mark^#(X2)	(96)
mark^#(first(X1,X2))	→	mark^#(X1)	(75)
mark^#(add(X1,X2))	→	mark^#(X2)	(122)
mark^#(terms(X))	→	mark^#(X)	(95)
mark^#(half(X))	→	mark^#(X)	(123)
active^#(first(s(X),cons(Y,Z)))	→	mark^#(cons(Y,first(X,Z)))	(130)
active^#(half(dbl(X)))	→	mark^#(X)	(93)
active^#(add(0,X))	→	mark^#(X)	(88)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(s(X))	→	mark^#(X)	(50)
active^#(sqr(s(X)))	→	mark^#(s(add(sqr(X),dbl(X))))	(121)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(94)
mark^#(sqr(X))	→	active^#(sqr(mark(X)))	(72)
mark^#(first(X1,X2))	→	active^#(first(mark(X1),mark(X2)))	(97)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(51)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(59)
mark^#(add(X1,X2))	→	mark^#(X1)	(53)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(104)
mark^#(terms(X))	→	active^#(terms(mark(X)))	(109)
active^#(half(s(s(X))))	→	mark^#(s(half(X)))	(81)
mark^#(half(X))	→	active^#(half(mark(X)))	(117)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	9711
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	31599
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	31599
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	31599
[0]	=	1
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[first(x₁, x₂)]	=	31598
[active(x₁)]	=	0
[cons(x₁, x₂)]	=	10451
[active^#(x₁)]	=	x₁ + 0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	31599
[sqr(x₁)]	=	31599
[terms(x₁)]	=	20585

together with the usable rules

s(active(X))	→	s(X)	(36)
terms(active(X))	→	terms(X)	(26)
recip(active(X))	→	recip(X)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
sqr(active(X))	→	sqr(X)	(34)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
first(X1,mark(X2))	→	first(X1,X2)	(44)
sqr(mark(X))	→	sqr(X)	(33)
add(active(X1),X2)	→	add(X1,X2)	(39)
terms(mark(X))	→	terms(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
recip(mark(X))	→	recip(X)	(31)
first(active(X1),X2)	→	first(X1,X2)	(45)
add(X1,active(X2))	→	add(X1,X2)	(40)
add(X1,mark(X2))	→	add(X1,X2)	(38)
half(active(X))	→	half(X)	(48)
half(mark(X))	→	half(X)	(47)
add(mark(X1),X2)	→	add(X1,X2)	(37)
dbl(mark(X))	→	dbl(X)	(41)
dbl(active(X))	→	dbl(X)	(42)
first(X1,active(X2))	→	first(X1,X2)	(46)
s(mark(X))	→	s(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)
first(mark(X1),X2)	→	first(X1,X2)	(43)

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

mark^#(first(X1,X2))	→	active^#(first(mark(X1),mark(X2)))	(97)
mark^#(terms(X))	→	active^#(terms(mark(X)))	(109)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(s(X))	→	mark^#(X)	(50)
active^#(sqr(s(X)))	→	mark^#(s(add(sqr(X),dbl(X))))	(121)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(94)
mark^#(sqr(X))	→	active^#(sqr(mark(X)))	(72)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(51)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(59)
mark^#(add(X1,X2))	→	mark^#(X1)	(53)
mark^#(add(X1,X2))	→	active^#(add(mark(X1),mark(X2)))	(104)
active^#(half(s(s(X))))	→	mark^#(s(half(X)))	(81)
mark^#(half(X))	→	active^#(half(mark(X)))	(117)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	1
π(recip)	=	1
π(half)	=	1
π(mark^#)	=	1
π(mark)	=	1
π(active)	=	1
π(active^#)	=	1

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

prec(s)	=	0	status(s)	=	[1]	list-extension(s)	=	Lex
prec(recip^#)	=	0	status(recip^#)	=	[]	list-extension(recip^#)	=	Lex
prec(dbl)	=	1	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(terms^#)	=	0	status(terms^#)	=	[]	list-extension(terms^#)	=	Lex
prec(half^#)	=	0	status(half^#)	=	[]	list-extension(half^#)	=	Lex
prec(sqr^#)	=	0	status(sqr^#)	=	[]	list-extension(sqr^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(first^#)	=	0	status(first^#)	=	[1, 2]	list-extension(first^#)	=	Lex
prec(nil)	=	3	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(first)	=	3	status(first)	=	[2, 1]	list-extension(first)	=	Lex
prec(cons)	=	3	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(add^#)	=	0	status(add^#)	=	[]	list-extension(add^#)	=	Lex
prec(add)	=	3	status(add)	=	[1, 2]	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
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[sqr^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[nil]	=	0
[first(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[cons(x₁, x₂)]	=	max(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

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

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

mark^#(s(X))	→	mark^#(X)	(50)
active^#(sqr(s(X)))	→	mark^#(s(add(sqr(X),dbl(X))))	(121)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(51)
active^#(add(s(X),Y))	→	mark^#(s(add(X,Y)))	(59)
mark^#(add(X1,X2))	→	mark^#(X1)	(53)
active^#(half(s(s(X))))	→	mark^#(s(half(X)))	(81)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

add^#(mark(X1),X2)	→	add^#(X1,X2)	(129)
add^#(X1,mark(X2))	→	add^#(X1,X2)	(78)
add^#(X1,active(X2))	→	add^#(X1,X2)	(76)
add^#(active(X1),X2)	→	add^#(X1,X2)	(74)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 7210
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	28938
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₂ + 0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
s(mark(X))	→	s(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

add^#(X1,mark(X2))	→	add^#(X1,X2)	(78)
add^#(X1,active(X2))	→	add^#(X1,X2)	(76)

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

add^#(active(X1),X2)	→	add^#(X1,X2)	(74)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(129)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 43950
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	49364
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 24324
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 28938
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

add^#(active(X1),X2)	→	add^#(X1,X2)	(74)
add^#(mark(X1),X2)	→	add^#(X1,X2)	(129)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

dbl^#(active(X))	→	dbl^#(X)	(70)
dbl^#(mark(X))	→	dbl^#(X)	(100)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 43950
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	x₁ + 0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	46797
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 14459
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 40578
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

dbl^#(active(X))	→	dbl^#(X)	(70)
dbl^#(mark(X))	→	dbl^#(X)	(100)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(89)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(128)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(125)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(64)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + x₂ + 0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 32576
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 38541
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	14457
[mark(x₁)]	=	x₁ + 38544
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 27846
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(89)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(128)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(125)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(64)

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

recip^#(mark(X))	→	recip^#(X)	(113)
recip^#(active(X))	→	recip^#(X)	(67)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 20067
[recip^#(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	36495
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

recip^#(mark(X))	→	recip^#(X)	(113)
recip^#(active(X))	→	recip^#(X)	(67)

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

sqr^#(active(X))	→	sqr^#(X)	(62)
sqr^#(mark(X))	→	sqr^#(X)	(57)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 9884
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 19560
[sqr^#(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	36495
[mark(x₁)]	=	x₁ + 19563
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 27644
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

sqr^#(active(X))	→	sqr^#(X)	(62)
sqr^#(mark(X))	→	sqr^#(X)	(57)

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

terms^#(mark(X))	→	terms^#(X)	(116)
terms^#(active(X))	→	terms^#(X)	(114)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 31413
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	x₁ + 0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 32647
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	47313
[mark(x₁)]	=	x₁ + 32650
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 27644
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

terms^#(mark(X))	→	terms^#(X)	(116)
terms^#(active(X))	→	terms^#(X)	(114)

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

s^#(mark(X))	→	s^#(X)	(131)
s^#(active(X))	→	s^#(X)	(68)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 28038
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	x₁ + 0
[first^#(x₁, x₂)]	=	0
[nil]	=	50917
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

s^#(mark(X))	→	s^#(X)	(131)
s^#(active(X))	→	s^#(X)	(68)

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

first^#(active(X1),X2)	→	first^#(X1,X2)	(83)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(61)
first^#(X1,active(X2))	→	first^#(X1,X2)	(106)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(49)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 21270
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	x₁ + x₂ + 0
[nil]	=	50917
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

first^#(active(X1),X2)	→	first^#(X1,X2)	(83)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(61)
first^#(X1,active(X2))	→	first^#(X1,X2)	(106)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(49)

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

half^#(mark(X))	→	half^#(X)	(77)
half^#(active(X))	→	half^#(X)	(102)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[recip(x₁)]	=	x₁ + 19510
[recip^#(x₁)]	=	0
[dbl(x₁)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[terms^#(x₁)]	=	0
[half^#(x₁)]	=	x₁ + 0
[half(x₁)]	=	x₁ + 1
[sqr^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	45181
[mark(x₁)]	=	x₁ + 4
[first(x₁, x₂)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 24054
[active^#(x₁)]	=	0
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[sqr(x₁)]	=	1
[terms(x₁)]	=	x₁ + 0

together with the usable rules

s(active(X))	→	s(X)	(36)
s(mark(X))	→	s(X)	(35)

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

half^#(mark(X))	→	half^#(X)	(77)
half^#(active(X))	→	half^#(X)	(102)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.