Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExAppendixB_AEL03_GM)

The rewrite relation of the following TRS is considered.

a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(0,Z)	→	rnil	(2)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
a__2ndsneg(0,Z)	→	rnil	(5)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__plus(0,Y)	→	mark(Y)	(9)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__times(0,Y)	→	0	(11)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
mark(from(X))	→	a__from(mark(X))	(14)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
mark(square(X))	→	a__square(mark(X))	(20)
mark(0)	→	0	(21)
mark(s(X))	→	s(mark(X))	(22)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
mark(nil)	→	nil	(25)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
mark(rnil)	→	rnil	(28)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__from(X)	→	from(X)	(30)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
a__pi(X)	→	pi(X)	(33)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
a__times(X1,X2)	→	times(X1,X2)	(35)
a__square(X)	→	square(X)	(36)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)
a__pi^#(X)	→	a__2ndspos^#(mark(X),a__from(0))	(38)
mark^#(cons2(X1,X2))	→	mark^#(X2)	(39)
mark^#(cons(X1,X2))	→	mark^#(X1)	(40)
mark^#(2ndspos(X1,X2))	→	a__2ndspos^#(mark(X1),mark(X2))	(41)
a__from^#(X)	→	mark^#(X)	(42)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(Z)	(43)
mark^#(2ndsneg(X1,X2))	→	mark^#(X1)	(44)
mark^#(2ndspos(X1,X2))	→	mark^#(X1)	(45)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
mark^#(2ndspos(X1,X2))	→	mark^#(X2)	(47)
mark^#(2ndsneg(X1,X2))	→	mark^#(X2)	(48)
a__square^#(X)	→	a__times^#(mark(X),mark(X))	(49)
mark^#(plus(X1,X2))	→	mark^#(X2)	(50)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(N)	(51)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(52)
a__times^#(s(X),Y)	→	mark^#(Y)	(53)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
mark^#(posrecip(X))	→	mark^#(X)	(55)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(56)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(57)
a__pi^#(X)	→	a__from^#(0)	(58)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
mark^#(pi(X))	→	mark^#(X)	(60)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(61)
mark^#(pi(X))	→	a__pi^#(mark(X))	(62)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(63)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(64)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(65)
mark^#(square(X))	→	mark^#(X)	(66)
a__square^#(X)	→	mark^#(X)	(67)
a__2ndspos^#(s(N),cons(X,Z))	→	a__2ndspos^#(s(mark(N)),cons2(X,mark(Z)))	(68)
mark^#(negrecip(X))	→	mark^#(X)	(69)
mark^#(times(X1,X2))	→	mark^#(X1)	(70)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(Z)	(71)
a__pi^#(X)	→	mark^#(X)	(72)
mark^#(s(X))	→	mark^#(X)	(73)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndspos^#(mark(N),mark(Z))	(74)
mark^#(times(X1,X2))	→	mark^#(X2)	(75)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
mark^#(from(X))	→	a__from^#(mark(X))	(77)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(square(X))	→	a__square^#(mark(X))	(79)
a__plus^#(s(X),Y)	→	mark^#(X)	(80)
mark^#(2ndsneg(X1,X2))	→	a__2ndsneg^#(mark(X1),mark(X2))	(81)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(82)
a__times^#(s(X),Y)	→	mark^#(Y)	(53)
a__2ndsneg^#(s(N),cons(X,Z))	→	a__2ndsneg^#(s(mark(N)),cons2(X,mark(Z)))	(83)
mark^#(rcons(X1,X2))	→	mark^#(X1)	(84)
mark^#(plus(X1,X2))	→	mark^#(X1)	(85)
a__square^#(X)	→	mark^#(X)	(67)
a__times^#(s(X),Y)	→	mark^#(X)	(86)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(N)	(87)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndsneg^#(mark(N),mark(Z))	(88)
mark^#(from(X))	→	mark^#(X)	(89)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(from(X))	→	mark^#(X)	(89)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndsneg^#(mark(N),mark(Z))	(88)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(65)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(63)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(64)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(N)	(87)
mark^#(pi(X))	→	a__pi^#(mark(X))	(62)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(61)
a__times^#(s(X),Y)	→	mark^#(X)	(86)
mark^#(pi(X))	→	mark^#(X)	(60)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
a__square^#(X)	→	mark^#(X)	(67)
a__pi^#(X)	→	a__from^#(0)	(58)
mark^#(plus(X1,X2))	→	mark^#(X1)	(85)
mark^#(rcons(X1,X2))	→	mark^#(X1)	(84)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(57)
a__2ndsneg^#(s(N),cons(X,Z))	→	a__2ndsneg^#(s(mark(N)),cons2(X,mark(Z)))	(83)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(56)
a__times^#(s(X),Y)	→	mark^#(Y)	(53)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(82)
mark^#(2ndsneg(X1,X2))	→	a__2ndsneg^#(mark(X1),mark(X2))	(81)
a__plus^#(s(X),Y)	→	mark^#(X)	(80)
mark^#(posrecip(X))	→	mark^#(X)	(55)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
a__times^#(s(X),Y)	→	mark^#(Y)	(53)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(52)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(square(X))	→	a__square^#(mark(X))	(79)
mark^#(from(X))	→	a__from^#(mark(X))	(77)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(N)	(51)
mark^#(plus(X1,X2))	→	mark^#(X2)	(50)
a__square^#(X)	→	a__times^#(mark(X),mark(X))	(49)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
mark^#(2ndsneg(X1,X2))	→	mark^#(X2)	(48)
mark^#(times(X1,X2))	→	mark^#(X2)	(75)
mark^#(2ndspos(X1,X2))	→	mark^#(X2)	(47)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndspos^#(mark(N),mark(Z))	(74)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
mark^#(s(X))	→	mark^#(X)	(73)
mark^#(2ndspos(X1,X2))	→	mark^#(X1)	(45)
a__pi^#(X)	→	mark^#(X)	(72)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(Z)	(71)
mark^#(2ndsneg(X1,X2))	→	mark^#(X1)	(44)
mark^#(times(X1,X2))	→	mark^#(X1)	(70)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(Z)	(43)
a__from^#(X)	→	mark^#(X)	(42)
mark^#(negrecip(X))	→	mark^#(X)	(69)
mark^#(2ndspos(X1,X2))	→	a__2ndspos^#(mark(X1),mark(X2))	(41)
a__2ndspos^#(s(N),cons(X,Z))	→	a__2ndspos^#(s(mark(N)),cons2(X,mark(Z)))	(68)
a__square^#(X)	→	mark^#(X)	(67)
mark^#(cons(X1,X2))	→	mark^#(X1)	(40)
mark^#(cons2(X1,X2))	→	mark^#(X2)	(39)
a__pi^#(X)	→	a__2ndspos^#(mark(X),a__from(0))	(38)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)
mark^#(square(X))	→	mark^#(X)	(66)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[negrecip(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	x₁ + 3
[a__from^#(x₁)]	=	x₁ + 1
[2ndspos(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[a__from(x₁)]	=	x₁ + 0
[rnil]	=	2
[square(x₁)]	=	x₁ + 2
[a__times^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[pi(x₁)]	=	x₁ + 2
[rcons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[a__2ndsneg^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[mark^#(x₁)]	=	x₁ + 1
[0]	=	1
[from(x₁)]	=	x₁ + 0
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[a__pi(x₁)]	=	x₁ + 2
[nil]	=	35102
[mark(x₁)]	=	x₁ + 0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[cons2(x₁, x₂)]	=	max(x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[a__square^#(x₁)]	=	x₁ + 3
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[posrecip(x₁)]	=	x₁ + 0

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

mark^#(pi(X))	→	mark^#(X)	(60)
a__square^#(X)	→	mark^#(X)	(67)
a__pi^#(X)	→	a__from^#(0)	(58)
a__times^#(s(X),Y)	→	mark^#(Y)	(53)
a__times^#(s(X),Y)	→	mark^#(Y)	(53)
a__square^#(X)	→	a__times^#(mark(X),mark(X))	(49)
mark^#(times(X1,X2))	→	mark^#(X2)	(75)
mark^#(2ndspos(X1,X2))	→	mark^#(X1)	(45)
a__pi^#(X)	→	mark^#(X)	(72)
mark^#(2ndsneg(X1,X2))	→	mark^#(X1)	(44)
a__square^#(X)	→	mark^#(X)	(67)
a__pi^#(X)	→	a__2ndspos^#(mark(X),a__from(0))	(38)
mark^#(square(X))	→	mark^#(X)	(66)

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^#(plus(X1,X2))	→	mark^#(X2)	(50)
mark^#(plus(X1,X2))	→	mark^#(X1)	(85)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(63)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(52)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndsneg^#(mark(N),mark(Z))	(88)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(64)
mark^#(2ndspos(X1,X2))	→	mark^#(X2)	(47)
mark^#(2ndspos(X1,X2))	→	a__2ndspos^#(mark(X1),mark(X2))	(41)
a__from^#(X)	→	mark^#(X)	(42)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(Z)	(43)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(N)	(51)
a__2ndspos^#(s(N),cons(X,Z))	→	a__2ndspos^#(s(mark(N)),cons2(X,mark(Z)))	(68)
mark^#(2ndsneg(X1,X2))	→	mark^#(X2)	(48)
mark^#(2ndsneg(X1,X2))	→	a__2ndsneg^#(mark(X1),mark(X2))	(81)
mark^#(cons(X1,X2))	→	mark^#(X1)	(40)
mark^#(times(X1,X2))	→	mark^#(X1)	(70)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(cons2(X1,X2))	→	mark^#(X2)	(39)
mark^#(s(X))	→	mark^#(X)	(73)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
a__plus^#(s(X),Y)	→	mark^#(X)	(80)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(65)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(56)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(57)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndspos^#(mark(N),mark(Z))	(74)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(82)
mark^#(from(X))	→	mark^#(X)	(89)
mark^#(from(X))	→	a__from^#(mark(X))	(77)
a__times^#(s(X),Y)	→	mark^#(X)	(86)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(61)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
mark^#(posrecip(X))	→	mark^#(X)	(55)
mark^#(negrecip(X))	→	mark^#(X)	(69)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(Z)	(71)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(N)	(87)
a__2ndsneg^#(s(N),cons(X,Z))	→	a__2ndsneg^#(s(mark(N)),cons2(X,mark(Z)))	(83)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)
mark^#(rcons(X1,X2))	→	mark^#(X1)	(84)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 13509, x₂ + 13508, 0)
[negrecip(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	x₁ + 3
[a__from^#(x₁)]	=	x₁ + 26721
[2ndspos(x₁, x₂)]	=	max(x₁ + 13509, x₂ + 13508, 0)
[a__from(x₁)]	=	x₁ + 11651
[rnil]	=	20686
[square(x₁)]	=	x₁ + 12330
[a__times^#(x₁, x₂)]	=	max(x₁ + 26720, x₂ + 39050, 0)
[pi(x₁)]	=	x₁ + 32336
[rcons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₁ + 13509, x₂ + 13508, 0)
[a__2ndsneg^#(x₁, x₂)]	=	max(x₁ + 26721, x₂ + 26722, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 26720, x₂ + 26720, 0)
[mark^#(x₁)]	=	x₁ + 26720
[0]	=	7177
[from(x₁)]	=	x₁ + 11651
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 12330, 0)
[a__pi(x₁)]	=	x₁ + 32336
[nil]	=	35102
[mark(x₁)]	=	x₁ + 0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 13509, x₂ + 13508, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[cons2(x₁, x₂)]	=	max(x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 12330
[cons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 12330, 0)
[a__square^#(x₁)]	=	x₁ + 3
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 26721, x₂ + 26722, 0)
[posrecip(x₁)]	=	x₁ + 0

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(63)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(52)
a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(64)
mark^#(2ndspos(X1,X2))	→	mark^#(X2)	(47)
mark^#(2ndspos(X1,X2))	→	a__2ndspos^#(mark(X1),mark(X2))	(41)
a__from^#(X)	→	mark^#(X)	(42)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(Z)	(43)
a__2ndspos^#(s(N),cons(X,Z))	→	mark^#(N)	(51)
mark^#(2ndsneg(X1,X2))	→	mark^#(X2)	(48)
mark^#(2ndsneg(X1,X2))	→	a__2ndsneg^#(mark(X1),mark(X2))	(81)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Z)	(56)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(N)	(57)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	mark^#(Y)	(82)
mark^#(from(X))	→	mark^#(X)	(89)
mark^#(from(X))	→	a__from^#(mark(X))	(77)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(Z)	(71)
a__2ndsneg^#(s(N),cons(X,Z))	→	mark^#(N)	(87)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndsneg^#(mark(N),mark(Z))	(88)
a__2ndspos^#(s(N),cons(X,Z))	→	a__2ndspos^#(s(mark(N)),cons2(X,mark(Z)))	(68)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndspos^#(mark(N),mark(Z))	(74)
a__2ndsneg^#(s(N),cons(X,Z))	→	a__2ndsneg^#(s(mark(N)),cons2(X,mark(Z)))	(83)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(2ndspos)	=	1
π(a__from)	=	1
π(rcons)	=	1
π(a__2ndspos)	=	1
π(a__2ndsneg^#)	=	1
π(mark^#)	=	1
π(from)	=	1
π(mark)	=	1
π(cons2)	=	1
π(cons)	=	1

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

prec(a__plus)	=	7	status(a__plus)	=	[2, 1]	list-extension(a__plus)	=	Lex
prec(a__2ndsneg)	=	2	status(a__2ndsneg)	=	[1, 2]	list-extension(a__2ndsneg)	=	Lex
prec(negrecip)	=	1	status(negrecip)	=	[]	list-extension(negrecip)	=	Lex
prec(s)	=	6	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__pi^#)	=	0	status(a__pi^#)	=	[]	list-extension(a__pi^#)	=	Lex
prec(a__from^#)	=	0	status(a__from^#)	=	[]	list-extension(a__from^#)	=	Lex
prec(rnil)	=	2	status(rnil)	=	[]	list-extension(rnil)	=	Lex
prec(square)	=	9	status(square)	=	[1]	list-extension(square)	=	Lex
prec(a__times^#)	=	0	status(a__times^#)	=	[2, 1]	list-extension(a__times^#)	=	Lex
prec(pi)	=	2	status(pi)	=	[1]	list-extension(pi)	=	Lex
prec(a__plus^#)	=	0	status(a__plus^#)	=	[2, 1]	list-extension(a__plus^#)	=	Lex
prec(0)	=	2	status(0)	=	[]	list-extension(0)	=	Lex
prec(times)	=	8	status(times)	=	[2, 1]	list-extension(times)	=	Lex
prec(a__pi)	=	2	status(a__pi)	=	[1]	list-extension(a__pi)	=	Lex
prec(nil)	=	3	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2ndsneg)	=	2	status(2ndsneg)	=	[1, 2]	list-extension(2ndsneg)	=	Lex
prec(plus)	=	7	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(a__square)	=	9	status(a__square)	=	[1]	list-extension(a__square)	=	Lex
prec(a__times)	=	8	status(a__times)	=	[2, 1]	list-extension(a__times)	=	Lex
prec(a__square^#)	=	0	status(a__square^#)	=	[]	list-extension(a__square^#)	=	Lex
prec(a__2ndspos^#)	=	2	status(a__2ndspos^#)	=	[1]	list-extension(a__2ndspos^#)	=	Lex
prec(posrecip)	=	6	status(posrecip)	=	[]	list-extension(posrecip)	=	Lex

and the following Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	0
[rnil]	=	0
[square(x₁)]	=	x₁ + 0
[a__times^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[pi(x₁)]	=	x₁ + 0
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[0]	=	0
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__pi(x₁)]	=	x₁ + 0
[nil]	=	0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 0
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square^#(x₁)]	=	0
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[posrecip(x₁)]	=	0

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

a__2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndsneg^#(mark(N),mark(Z))	(88)
a__2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	a__2ndspos^#(mark(N),mark(Z))	(74)

could be deleted.

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

mark^#(plus(X1,X2))	→	mark^#(X2)	(50)
mark^#(plus(X1,X2))	→	mark^#(X1)	(85)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
mark^#(cons(X1,X2))	→	mark^#(X1)	(40)
mark^#(times(X1,X2))	→	mark^#(X1)	(70)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(cons2(X1,X2))	→	mark^#(X2)	(39)
mark^#(s(X))	→	mark^#(X)	(73)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
a__plus^#(s(X),Y)	→	mark^#(X)	(80)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(65)
a__times^#(s(X),Y)	→	mark^#(X)	(86)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(61)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
mark^#(posrecip(X))	→	mark^#(X)	(55)
mark^#(negrecip(X))	→	mark^#(X)	(69)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)
mark^#(rcons(X1,X2))	→	mark^#(X1)	(84)

1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₂ + 1, 0)
[negrecip(x₁)]	=	x₁ + 12444
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	3
[a__from^#(x₁)]	=	26721
[2ndspos(x₁, x₂)]	=	max(x₂ + 1, 0)
[a__from(x₁)]	=	x₁ + 12444
[rnil]	=	1
[square(x₁)]	=	x₁ + 10750
[a__times^#(x₁, x₂)]	=	max(x₁ + 36557, x₂ + 25809, 0)
[pi(x₁)]	=	13510
[rcons(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₂ + 1, 0)
[a__2ndsneg^#(x₁, x₂)]	=	max(0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 25808, x₂ + 25807, 0)
[mark^#(x₁)]	=	x₁ + 25807
[0]	=	201
[from(x₁)]	=	x₁ + 12444
[times(x₁, x₂)]	=	max(x₁ + 10750, x₂ + 2, 0)
[a__pi(x₁)]	=	13510
[nil]	=	16512
[mark(x₁)]	=	x₁ + 0
[2ndsneg(x₁, x₂)]	=	max(x₂ + 1, 0)
[plus(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[cons2(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 10750
[cons(x₁, x₂)]	=	max(x₁ + 12444, x₂ + 0, 0)
[a__times(x₁, x₂)]	=	max(x₁ + 10750, x₂ + 2, 0)
[a__square^#(x₁)]	=	3
[a__2ndspos^#(x₁, x₂)]	=	max(0)
[posrecip(x₁)]	=	x₁ + 2331

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

mark^#(plus(X1,X2))	→	mark^#(X1)	(85)
mark^#(cons(X1,X2))	→	mark^#(X1)	(40)
mark^#(times(X1,X2))	→	mark^#(X1)	(70)
a__plus^#(s(X),Y)	→	mark^#(X)	(80)
a__times^#(s(X),Y)	→	mark^#(X)	(86)
mark^#(posrecip(X))	→	mark^#(X)	(55)
mark^#(negrecip(X))	→	mark^#(X)	(69)
mark^#(rcons(X1,X2))	→	mark^#(X1)	(84)

could be deleted.

1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(plus(X1,X2))	→	mark^#(X2)	(50)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(cons2(X1,X2))	→	mark^#(X2)	(39)
mark^#(s(X))	→	mark^#(X)	(73)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(65)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(61)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)

1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₂ + 0
[a__2ndsneg(x₁, x₂)]	=	1
[negrecip(x₁)]	=	1
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	2
[2ndspos(x₁, x₂)]	=	1
[a__from(x₁)]	=	1
[rnil]	=	1
[square(x₁)]	=	x₁ + 36130
[a__times^#(x₁, x₂)]	=	0
[pi(x₁)]	=	40911
[rcons(x₁, x₂)]	=	x₂ + 0
[a__2ndspos(x₁, x₂)]	=	1
[a__2ndsneg^#(x₁, x₂)]	=	0
[a__plus^#(x₁, x₂)]	=	x₂ + 0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[from(x₁)]	=	1
[times(x₁, x₂)]	=	0
[a__pi(x₁)]	=	40911
[nil]	=	35676
[mark(x₁)]	=	x₁ + 0
[2ndsneg(x₁, x₂)]	=	1
[plus(x₁, x₂)]	=	x₂ + 0
[cons2(x₁, x₂)]	=	x₂ + 27072
[a__square(x₁)]	=	x₁ + 36130
[cons(x₁, x₂)]	=	1
[a__times(x₁, x₂)]	=	0
[a__square^#(x₁)]	=	0
[a__2ndspos^#(x₁, x₂)]	=	0
[posrecip(x₁)]	=	8702

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

mark^#(cons2(X1,X2))

→

mark^#(X2)

(39)

could be deleted.

1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(plus(X1,X2))	→	mark^#(X2)	(50)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(s(X))	→	mark^#(X)	(73)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(65)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(61)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)

1.1.1.1.1.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__from)	=	1
π(a__2ndsneg^#)	=	1
π(from)	=	1
π(mark)	=	1
π(cons2)	=	1
π(cons)	=	1

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

prec(a__plus)	=	8	status(a__plus)	=	[2, 1]	list-extension(a__plus)	=	Lex
prec(a__2ndsneg)	=	1	status(a__2ndsneg)	=	[1]	list-extension(a__2ndsneg)	=	Lex
prec(negrecip)	=	0	status(negrecip)	=	[]	list-extension(negrecip)	=	Lex
prec(s)	=	6	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__pi^#)	=	0	status(a__pi^#)	=	[]	list-extension(a__pi^#)	=	Lex
prec(a__from^#)	=	0	status(a__from^#)	=	[]	list-extension(a__from^#)	=	Lex
prec(2ndspos)	=	2	status(2ndspos)	=	[1]	list-extension(2ndspos)	=	Lex
prec(rnil)	=	1	status(rnil)	=	[]	list-extension(rnil)	=	Lex
prec(square)	=	10	status(square)	=	[1]	list-extension(square)	=	Lex
prec(a__times^#)	=	9	status(a__times^#)	=	[2, 1]	list-extension(a__times^#)	=	Lex
prec(pi)	=	3	status(pi)	=	[1]	list-extension(pi)	=	Lex
prec(rcons)	=	2	status(rcons)	=	[1, 2]	list-extension(rcons)	=	Lex
prec(a__2ndspos)	=	2	status(a__2ndspos)	=	[1]	list-extension(a__2ndspos)	=	Lex
prec(a__plus^#)	=	7	status(a__plus^#)	=	[1, 2]	list-extension(a__plus^#)	=	Lex
prec(mark^#)	=	4	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(times)	=	9	status(times)	=	[2, 1]	list-extension(times)	=	Lex
prec(a__pi)	=	3	status(a__pi)	=	[1]	list-extension(a__pi)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2ndsneg)	=	1	status(2ndsneg)	=	[1]	list-extension(2ndsneg)	=	Lex
prec(plus)	=	8	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(a__square)	=	10	status(a__square)	=	[1]	list-extension(a__square)	=	Lex
prec(a__times)	=	9	status(a__times)	=	[2, 1]	list-extension(a__times)	=	Lex
prec(a__square^#)	=	0	status(a__square^#)	=	[]	list-extension(a__square^#)	=	Lex
prec(a__2ndspos^#)	=	2	status(a__2ndspos^#)	=	[1]	list-extension(a__2ndspos^#)	=	Lex
prec(posrecip)	=	6	status(posrecip)	=	[]	list-extension(posrecip)	=	Lex

and the following Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 0, 0)
[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	0
[2ndspos(x₁, x₂)]	=	max(x₁ + 0, 0)
[rnil]	=	0
[square(x₁)]	=	x₁ + 0
[a__times^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[pi(x₁)]	=	x₁ + 0
[rcons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__pi(x₁)]	=	x₁ + 0
[nil]	=	0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 0
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square^#(x₁)]	=	0
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[posrecip(x₁)]	=	0

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

mark^#(plus(X1,X2))	→	mark^#(X2)	(50)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(46)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(78)
mark^#(s(X))	→	mark^#(X)	(73)
a__plus^#(s(X),Y)	→	mark^#(Y)	(76)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(59)
a__plus^#(0,Y)	→	mark^#(Y)	(54)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(37)

could be deleted.

1.1.1.1.1.1.2.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__plus^#(s(X),Y)

→

a__plus^#(mark(X),mark(Y))

(65)

1.1.1.1.1.1.2.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__from)	=	1
π(a__2ndsneg^#)	=	1
π(from)	=	1
π(mark)	=	1
π(cons2)	=	1
π(cons)	=	1

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

prec(a__plus)	=	8	status(a__plus)	=	[2, 1]	list-extension(a__plus)	=	Lex
prec(a__2ndsneg)	=	1	status(a__2ndsneg)	=	[1]	list-extension(a__2ndsneg)	=	Lex
prec(negrecip)	=	0	status(negrecip)	=	[]	list-extension(negrecip)	=	Lex
prec(s)	=	6	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__pi^#)	=	0	status(a__pi^#)	=	[]	list-extension(a__pi^#)	=	Lex
prec(a__from^#)	=	0	status(a__from^#)	=	[]	list-extension(a__from^#)	=	Lex
prec(2ndspos)	=	2	status(2ndspos)	=	[1]	list-extension(2ndspos)	=	Lex
prec(rnil)	=	1	status(rnil)	=	[]	list-extension(rnil)	=	Lex
prec(square)	=	10	status(square)	=	[1]	list-extension(square)	=	Lex
prec(a__times^#)	=	9	status(a__times^#)	=	[2, 1]	list-extension(a__times^#)	=	Lex
prec(pi)	=	3	status(pi)	=	[1]	list-extension(pi)	=	Lex
prec(rcons)	=	2	status(rcons)	=	[1, 2]	list-extension(rcons)	=	Lex
prec(a__2ndspos)	=	2	status(a__2ndspos)	=	[1]	list-extension(a__2ndspos)	=	Lex
prec(a__plus^#)	=	7	status(a__plus^#)	=	[1, 2]	list-extension(a__plus^#)	=	Lex
prec(mark^#)	=	4	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(times)	=	9	status(times)	=	[2, 1]	list-extension(times)	=	Lex
prec(a__pi)	=	3	status(a__pi)	=	[1]	list-extension(a__pi)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2ndsneg)	=	1	status(2ndsneg)	=	[1]	list-extension(2ndsneg)	=	Lex
prec(plus)	=	8	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(a__square)	=	10	status(a__square)	=	[1]	list-extension(a__square)	=	Lex
prec(a__times)	=	9	status(a__times)	=	[2, 1]	list-extension(a__times)	=	Lex
prec(a__square^#)	=	0	status(a__square^#)	=	[]	list-extension(a__square^#)	=	Lex
prec(a__2ndspos^#)	=	2	status(a__2ndspos^#)	=	[1]	list-extension(a__2ndspos^#)	=	Lex
prec(posrecip)	=	6	status(posrecip)	=	[]	list-extension(posrecip)	=	Lex

and the following Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 0, 0)
[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	0
[2ndspos(x₁, x₂)]	=	max(x₁ + 0, 0)
[rnil]	=	0
[square(x₁)]	=	x₁ + 0
[a__times^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[pi(x₁)]	=	x₁ + 0
[rcons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__pi(x₁)]	=	x₁ + 0
[nil]	=	0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 0
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square^#(x₁)]	=	0
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[posrecip(x₁)]	=	0

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

a__plus^#(s(X),Y)

→

a__plus^#(mark(X),mark(Y))

(65)

could be deleted.

1.1.1.1.1.1.2.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

a__times^#(s(X),Y)

→

a__times^#(mark(X),mark(Y))

(61)

1.1.1.1.1.1.2.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__from)	=	1
π(a__2ndsneg^#)	=	1
π(from)	=	1
π(mark)	=	1
π(cons2)	=	1
π(cons)	=	1

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

prec(a__plus)	=	8	status(a__plus)	=	[2, 1]	list-extension(a__plus)	=	Lex
prec(a__2ndsneg)	=	1	status(a__2ndsneg)	=	[1]	list-extension(a__2ndsneg)	=	Lex
prec(negrecip)	=	0	status(negrecip)	=	[]	list-extension(negrecip)	=	Lex
prec(s)	=	6	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__pi^#)	=	0	status(a__pi^#)	=	[]	list-extension(a__pi^#)	=	Lex
prec(a__from^#)	=	0	status(a__from^#)	=	[]	list-extension(a__from^#)	=	Lex
prec(2ndspos)	=	2	status(2ndspos)	=	[1]	list-extension(2ndspos)	=	Lex
prec(rnil)	=	1	status(rnil)	=	[]	list-extension(rnil)	=	Lex
prec(square)	=	10	status(square)	=	[1]	list-extension(square)	=	Lex
prec(a__times^#)	=	2	status(a__times^#)	=	[2, 1]	list-extension(a__times^#)	=	Lex
prec(pi)	=	3	status(pi)	=	[1]	list-extension(pi)	=	Lex
prec(rcons)	=	2	status(rcons)	=	[1, 2]	list-extension(rcons)	=	Lex
prec(a__2ndspos)	=	2	status(a__2ndspos)	=	[1]	list-extension(a__2ndspos)	=	Lex
prec(a__plus^#)	=	7	status(a__plus^#)	=	[1, 2]	list-extension(a__plus^#)	=	Lex
prec(mark^#)	=	4	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(times)	=	9	status(times)	=	[2, 1]	list-extension(times)	=	Lex
prec(a__pi)	=	3	status(a__pi)	=	[1]	list-extension(a__pi)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2ndsneg)	=	1	status(2ndsneg)	=	[1]	list-extension(2ndsneg)	=	Lex
prec(plus)	=	8	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(a__square)	=	10	status(a__square)	=	[1]	list-extension(a__square)	=	Lex
prec(a__times)	=	9	status(a__times)	=	[2, 1]	list-extension(a__times)	=	Lex
prec(a__square^#)	=	0	status(a__square^#)	=	[]	list-extension(a__square^#)	=	Lex
prec(a__2ndspos^#)	=	2	status(a__2ndspos^#)	=	[1]	list-extension(a__2ndspos^#)	=	Lex
prec(posrecip)	=	6	status(posrecip)	=	[]	list-extension(posrecip)	=	Lex

and the following Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 0, 0)
[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	0
[2ndspos(x₁, x₂)]	=	max(x₁ + 0, 0)
[rnil]	=	0
[square(x₁)]	=	x₁ + 0
[a__times^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[pi(x₁)]	=	x₁ + 0
[rcons(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__pi(x₁)]	=	x₁ + 0
[nil]	=	0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 0
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square^#(x₁)]	=	0
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[posrecip(x₁)]	=	0

together with the usable rules

mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(18)
a__2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(4)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(15)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__2ndspos(s(N),cons(X,Z))	→	a__2ndspos(s(mark(N)),cons2(X,mark(Z)))	(3)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(16)
mark(0)	→	0	(21)
a__square(X)	→	square(X)	(36)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(26)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(19)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(32)
mark(pi(X))	→	a__pi(mark(X))	(17)
mark(cons2(X1,X2))	→	cons2(X1,mark(X2))	(27)
a__plus(X1,X2)	→	plus(X1,X2)	(34)
mark(s(X))	→	s(mark(X))	(22)
mark(rnil)	→	rnil	(28)
a__2ndsneg(0,Z)	→	rnil	(5)
a__pi(X)	→	pi(X)	(33)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(10)
a__2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(7)
mark(square(X))	→	a__square(mark(X))	(20)
mark(nil)	→	nil	(25)
a__from(X)	→	from(X)	(30)
mark(from(X))	→	a__from(mark(X))	(14)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(31)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(12)
mark(posrecip(X))	→	posrecip(mark(X))	(23)
mark(negrecip(X))	→	negrecip(mark(X))	(24)
a__times(0,Y)	→	0	(11)
a__plus(0,Y)	→	mark(Y)	(9)
a__square(X)	→	a__times(mark(X),mark(X))	(13)
a__2ndsneg(s(N),cons(X,Z))	→	a__2ndsneg(s(mark(N)),cons2(X,mark(Z)))	(6)
a__times(X1,X2)	→	times(X1,X2)	(35)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(29)
a__2ndspos(0,Z)	→	rnil	(2)

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

a__times^#(s(X),Y)

→

a__times^#(mark(X),mark(Y))

(61)

could be deleted.

1.1.1.1.1.1.2.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.