Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_2_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,cons(Y,Z)))	→	rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z)))	(3)
a__2ndsneg(0,Z)	→	rnil	(4)
a__2ndsneg(s(N),cons(X,cons(Y,Z)))	→	rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z)))	(5)
a__pi(X)	→	a__2ndspos(mark(X),a__from(0))	(6)
a__plus(0,Y)	→	mark(Y)	(7)
a__plus(s(X),Y)	→	s(a__plus(mark(X),mark(Y)))	(8)
a__times(0,Y)	→	0	(9)
a__times(s(X),Y)	→	a__plus(mark(Y),a__times(mark(X),mark(Y)))	(10)
a__square(X)	→	a__times(mark(X),mark(X))	(11)
mark(from(X))	→	a__from(mark(X))	(12)
mark(2ndspos(X1,X2))	→	a__2ndspos(mark(X1),mark(X2))	(13)
mark(2ndsneg(X1,X2))	→	a__2ndsneg(mark(X1),mark(X2))	(14)
mark(pi(X))	→	a__pi(mark(X))	(15)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(16)
mark(times(X1,X2))	→	a__times(mark(X1),mark(X2))	(17)
mark(square(X))	→	a__square(mark(X))	(18)
mark(0)	→	0	(19)
mark(s(X))	→	s(mark(X))	(20)
mark(posrecip(X))	→	posrecip(mark(X))	(21)
mark(negrecip(X))	→	negrecip(mark(X))	(22)
mark(nil)	→	nil	(23)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(24)
mark(rnil)	→	rnil	(25)
mark(rcons(X1,X2))	→	rcons(mark(X1),mark(X2))	(26)
a__from(X)	→	from(X)	(27)
a__2ndspos(X1,X2)	→	2ndspos(X1,X2)	(28)
a__2ndsneg(X1,X2)	→	2ndsneg(X1,X2)	(29)
a__pi(X)	→	pi(X)	(30)
a__plus(X1,X2)	→	plus(X1,X2)	(31)
a__times(X1,X2)	→	times(X1,X2)	(32)
a__square(X)	→	square(X)	(33)

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.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	max(x₁ + 14683, x₂ + 0, 0)
[a__2ndsneg(x₁, x₂)]	=	max(x₁ + 15927, x₂ + 15924, 0)
[negrecip(x₁)]	=	x₁ + 9983
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	x₁ + 82871
[a__from^#(x₁)]	=	x₁ + 4322
[2ndspos(x₁, x₂)]	=	max(x₁ + 15927, x₂ + 15924, 0)
[a__from(x₁)]	=	x₁ + 21657
[rnil]	=	15925
[square(x₁)]	=	x₁ + 49915
[a__times^#(x₁, x₂)]	=	max(x₁ + 19003, x₂ + 45289, 0)
[pi(x₁)]	=	x₁ + 78551
[rcons(x₁, x₂)]	=	max(x₁ + 5942, x₂ + 0, 0)
[a__2ndspos(x₁, x₂)]	=	max(x₁ + 15927, x₂ + 15924, 0)
[a__2ndsneg^#(x₁, x₂)]	=	max(x₁ + 20243, x₂ + 20244, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 4322, x₂ + 4321, 0)
[mark^#(x₁)]	=	x₁ + 4321
[0]	=	40969
[from(x₁)]	=	x₁ + 21657
[times(x₁, x₂)]	=	max(x₁ + 14682, x₂ + 40968, 0)
[a__pi(x₁)]	=	x₁ + 78551
[nil]	=	39434
[mark(x₁)]	=	x₁ + 0
[2ndsneg(x₁, x₂)]	=	max(x₁ + 15927, x₂ + 15924, 0)
[plus(x₁, x₂)]	=	max(x₁ + 14683, x₂ + 0, 0)
[a__square(x₁)]	=	x₁ + 49915
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[a__times(x₁, x₂)]	=	max(x₁ + 14682, x₂ + 40968, 0)
[a__square^#(x₁)]	=	x₁ + 45290
[a__2ndspos^#(x₁, x₂)]	=	max(x₁ + 20243, x₂ + 20244, 0)
[posrecip(x₁)]	=	x₁ + 9983

together with the usable rules

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

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

a__2ndsneg^#(s(N),cons(X,cons(Y,Z)))	→	mark^#(N)	(57)
mark^#(2ndspos(X1,X2))	→	a__2ndspos^#(mark(X1),mark(X2))	(78)
mark^#(times(X1,X2))	→	mark^#(X2)	(56)
mark^#(2ndsneg(X1,X2))	→	mark^#(X1)	(55)
mark^#(2ndsneg(X1,X2))	→	mark^#(X2)	(77)
mark^#(rcons(X1,X2))	→	mark^#(X1)	(54)
mark^#(from(X))	→	mark^#(X)	(53)
a__square^#(X)	→	mark^#(X)	(48)
mark^#(pi(X))	→	a__pi^#(mark(X))	(52)
a__pi^#(X)	→	a__2ndspos^#(mark(X),a__from(0))	(76)
a__2ndsneg^#(s(N),cons(X,cons(Y,Z)))	→	mark^#(Y)	(51)
a__pi^#(X)	→	a__from^#(0)	(75)
a__times^#(s(X),Y)	→	mark^#(X)	(73)
a__2ndsneg^#(s(N),cons(X,cons(Y,Z)))	→	mark^#(Z)	(71)
mark^#(from(X))	→	a__from^#(mark(X))	(49)
a__square^#(X)	→	mark^#(X)	(48)
mark^#(2ndsneg(X1,X2))	→	a__2ndsneg^#(mark(X1),mark(X2))	(47)
a__times^#(s(X),Y)	→	mark^#(Y)	(66)
a__2ndspos^#(s(N),cons(X,cons(Y,Z)))	→	mark^#(Z)	(46)
mark^#(2ndspos(X1,X2))	→	mark^#(X2)	(45)
mark^#(negrecip(X))	→	mark^#(X)	(68)
mark^#(square(X))	→	mark^#(X)	(43)
a__times^#(s(X),Y)	→	mark^#(Y)	(66)
mark^#(square(X))	→	a__square^#(mark(X))	(42)
mark^#(2ndspos(X1,X2))	→	mark^#(X1)	(63)
a__2ndspos^#(s(N),cons(X,cons(Y,Z)))	→	mark^#(Y)	(41)
mark^#(posrecip(X))	→	mark^#(X)	(62)
a__from^#(X)	→	mark^#(X)	(40)
mark^#(cons(X1,X2))	→	mark^#(X1)	(61)
mark^#(pi(X))	→	mark^#(X)	(38)
a__2ndspos^#(s(N),cons(X,cons(Y,Z)))	→	mark^#(N)	(60)
a__square^#(X)	→	a__times^#(mark(X),mark(X))	(59)
mark^#(plus(X1,X2))	→	mark^#(X1)	(37)
mark^#(times(X1,X2))	→	mark^#(X1)	(36)
a__plus^#(s(X),Y)	→	mark^#(X)	(35)
a__pi^#(X)	→	mark^#(X)	(34)

could be deleted.

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),cons(X,cons(Y,Z)))	→	a__2ndsneg^#(mark(N),mark(Z))	(44)
a__2ndsneg^#(s(N),cons(X,cons(Y,Z)))	→	a__2ndspos^#(mark(N),mark(Z))	(50)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(negrecip)	=	1
π(a__times^#)	=	1
π(mark^#)	=	1
π(mark)	=	1
π(a__2ndspos^#)	=	1

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

prec(a__plus)	=	5	status(a__plus)	=	[1, 2]	list-extension(a__plus)	=	Lex
prec(a__2ndsneg)	=	5	status(a__2ndsneg)	=	[1, 2]	list-extension(a__2ndsneg)	=	Lex
prec(s)	=	4	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)	=	[]	list-extension(2ndspos)	=	Lex
prec(a__from)	=	3	status(a__from)	=	[1]	list-extension(a__from)	=	Lex
prec(rnil)	=	2	status(rnil)	=	[]	list-extension(rnil)	=	Lex
prec(square)	=	7	status(square)	=	[1]	list-extension(square)	=	Lex
prec(pi)	=	6	status(pi)	=	[]	list-extension(pi)	=	Lex
prec(rcons)	=	1	status(rcons)	=	[]	list-extension(rcons)	=	Lex
prec(a__2ndspos)	=	2	status(a__2ndspos)	=	[]	list-extension(a__2ndspos)	=	Lex
prec(a__2ndsneg^#)	=	0	status(a__2ndsneg^#)	=	[1]	list-extension(a__2ndsneg^#)	=	Lex
prec(a__plus^#)	=	0	status(a__plus^#)	=	[2, 1]	list-extension(a__plus^#)	=	Lex
prec(0)	=	6	status(0)	=	[]	list-extension(0)	=	Lex
prec(from)	=	3	status(from)	=	[1]	list-extension(from)	=	Lex
prec(times)	=	6	status(times)	=	[1, 2]	list-extension(times)	=	Lex
prec(a__pi)	=	6	status(a__pi)	=	[]	list-extension(a__pi)	=	Lex
prec(nil)	=	2	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2ndsneg)	=	5	status(2ndsneg)	=	[1, 2]	list-extension(2ndsneg)	=	Lex
prec(plus)	=	5	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(a__square)	=	7	status(a__square)	=	[1]	list-extension(a__square)	=	Lex
prec(cons)	=	2	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(a__times)	=	6	status(a__times)	=	[1, 2]	list-extension(a__times)	=	Lex
prec(a__square^#)	=	0	status(a__square^#)	=	[]	list-extension(a__square^#)	=	Lex
prec(posrecip)	=	2	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)
[s(x₁)]	=	x₁ + 0
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	0
[2ndspos(x₁, x₂)]	=	max(0)
[a__from(x₁)]	=	x₁ + 0
[rnil]	=	0
[square(x₁)]	=	x₁ + 0
[pi(x₁)]	=	0
[rcons(x₁, x₂)]	=	max(0)
[a__2ndspos(x₁, x₂)]	=	max(0)
[a__2ndsneg^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[0]	=	0
[from(x₁)]	=	x₁ + 0
[times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__pi(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
[cons(x₁, x₂)]	=	max(0)
[a__times(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__square^#(x₁)]	=	0
[posrecip(x₁)]	=	0

together with the usable rules

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

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

a__plus^#(s(X),Y)	→	mark^#(Y)	(64)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(39)
mark^#(plus(X1,X2))	→	mark^#(X2)	(72)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(67)
mark^#(rcons(X1,X2))	→	mark^#(X2)	(70)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(65)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(58)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(79)
a__plus^#(0,Y)	→	mark^#(Y)	(69)
mark^#(s(X))	→	mark^#(X)	(74)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(rcons)	=	2
π(mark)	=	1
π(cons)	=	2
π(a__2ndspos^#)	=	1

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

prec(a__plus)	=	10	status(a__plus)	=	[2, 1]	list-extension(a__plus)	=	Lex
prec(a__2ndsneg)	=	5	status(a__2ndsneg)	=	[1, 2]	list-extension(a__2ndsneg)	=	Lex
prec(negrecip)	=	4	status(negrecip)	=	[]	list-extension(negrecip)	=	Lex
prec(s)	=	4	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)	=	5	status(2ndspos)	=	[1, 2]	list-extension(2ndspos)	=	Lex
prec(a__from)	=	3	status(a__from)	=	[]	list-extension(a__from)	=	Lex
prec(rnil)	=	5	status(rnil)	=	[]	list-extension(rnil)	=	Lex
prec(square)	=	12	status(square)	=	[1]	list-extension(square)	=	Lex
prec(a__times^#)	=	11	status(a__times^#)	=	[1, 2]	list-extension(a__times^#)	=	Lex
prec(pi)	=	6	status(pi)	=	[1]	list-extension(pi)	=	Lex
prec(a__2ndspos)	=	5	status(a__2ndspos)	=	[1, 2]	list-extension(a__2ndspos)	=	Lex
prec(a__2ndsneg^#)	=	0	status(a__2ndsneg^#)	=	[1]	list-extension(a__2ndsneg^#)	=	Lex
prec(a__plus^#)	=	9	status(a__plus^#)	=	[1, 2]	list-extension(a__plus^#)	=	Lex
prec(mark^#)	=	8	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(0)	=	7	status(0)	=	[]	list-extension(0)	=	Lex
prec(from)	=	3	status(from)	=	[]	list-extension(from)	=	Lex
prec(times)	=	11	status(times)	=	[1, 2]	list-extension(times)	=	Lex
prec(a__pi)	=	6	status(a__pi)	=	[1]	list-extension(a__pi)	=	Lex
prec(nil)	=	2	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2ndsneg)	=	5	status(2ndsneg)	=	[1, 2]	list-extension(2ndsneg)	=	Lex
prec(plus)	=	10	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(a__square)	=	12	status(a__square)	=	[1]	list-extension(a__square)	=	Lex
prec(a__times)	=	11	status(a__times)	=	[1, 2]	list-extension(a__times)	=	Lex
prec(a__square^#)	=	0	status(a__square^#)	=	[]	list-extension(a__square^#)	=	Lex
prec(posrecip)	=	2	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
[2ndspos(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 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__2ndspos(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__2ndsneg^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[from(x₁)]	=	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
[posrecip(x₁)]	=	0

together with the usable rules

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

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

a__plus^#(s(X),Y)	→	mark^#(Y)	(64)
a__plus^#(s(X),Y)	→	a__plus^#(mark(X),mark(Y))	(39)
mark^#(plus(X1,X2))	→	mark^#(X2)	(72)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(67)
mark^#(times(X1,X2))	→	a__times^#(mark(X1),mark(X2))	(65)
a__times^#(s(X),Y)	→	a__times^#(mark(X),mark(Y))	(58)
a__times^#(s(X),Y)	→	a__plus^#(mark(Y),a__times(mark(X),mark(Y)))	(79)
a__plus^#(0,Y)	→	mark^#(Y)	(69)
mark^#(s(X))	→	mark^#(X)	(74)

could be deleted.

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^#(rcons(X1,X2))

→

mark^#(X2)

(70)

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 0
[a__2ndsneg(x₁, x₂)]	=	21275
[negrecip(x₁)]	=	1
[s(x₁)]	=	x₁ + 8350
[a__pi^#(x₁)]	=	0
[a__from^#(x₁)]	=	0
[2ndspos(x₁, x₂)]	=	21277
[a__from(x₁)]	=	x₁ + 61389
[rnil]	=	40731
[square(x₁)]	=	4
[a__times^#(x₁, x₂)]	=	1
[pi(x₁)]	=	6
[rcons(x₁, x₂)]	=	x₂ + 2
[a__2ndspos(x₁, x₂)]	=	21276
[a__2ndsneg^#(x₁, x₂)]	=	0
[a__plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	3
[from(x₁)]	=	61388
[times(x₁, x₂)]	=	x₁ + 1
[a__pi(x₁)]	=	x₁ + 5
[nil]	=	32533
[mark(x₁)]	=	x₁ + 4
[2ndsneg(x₁, x₂)]	=	x₁ + x₂ + 21276
[plus(x₁, x₂)]	=	3
[a__square(x₁)]	=	x₁ + 5
[cons(x₁, x₂)]	=	61390
[a__times(x₁, x₂)]	=	x₂ + 2
[a__square^#(x₁)]	=	0
[a__2ndspos^#(x₁, x₂)]	=	1
[posrecip(x₁)]	=	29178

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

mark^#(rcons(X1,X2))

→

mark^#(X2)

(70)

could be deleted.

1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.