Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex49_GM04_iGM)

The rewrite relation of the following TRS is considered.

active(minus(0,Y))	→	mark(0)	(1)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(2)
active(geq(X,0))	→	mark(true)	(3)
active(geq(0,s(Y)))	→	mark(false)	(4)
active(geq(s(X),s(Y)))	→	mark(geq(X,Y))	(5)
active(div(0,s(Y)))	→	mark(0)	(6)
active(div(s(X),s(Y)))	→	mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(7)
active(if(true,X,Y))	→	mark(X)	(8)
active(if(false,X,Y))	→	mark(Y)	(9)
mark(minus(X1,X2))	→	active(minus(X1,X2))	(10)
mark(0)	→	active(0)	(11)
mark(s(X))	→	active(s(mark(X)))	(12)
mark(geq(X1,X2))	→	active(geq(X1,X2))	(13)
mark(true)	→	active(true)	(14)
mark(false)	→	active(false)	(15)
mark(div(X1,X2))	→	active(div(mark(X1),X2))	(16)
mark(if(X1,X2,X3))	→	active(if(mark(X1),X2,X3))	(17)
minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
s(mark(X))	→	s(X)	(22)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
div(mark(X1),X2)	→	div(X1,X2)	(28)
div(X1,mark(X2))	→	div(X1,X2)	(29)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)

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.

active^#(minus(s(X),s(Y)))	→	minus^#(X,Y)	(38)
mark^#(div(X1,X2))	→	div^#(mark(X1),X2)	(39)
active^#(geq(s(X),s(Y)))	→	geq^#(X,Y)	(40)
mark^#(if(X1,X2,X3))	→	if^#(mark(X1),X2,X3)	(41)
active^#(minus(0,Y))	→	mark^#(0)	(42)
mark^#(div(X1,X2))	→	active^#(div(mark(X1),X2))	(43)
minus^#(X1,active(X2))	→	minus^#(X1,X2)	(44)
if^#(mark(X1),X2,X3)	→	if^#(X1,X2,X3)	(45)
active^#(if(true,X,Y))	→	mark^#(X)	(46)
mark^#(false)	→	active^#(false)	(47)
minus^#(X1,mark(X2))	→	minus^#(X1,X2)	(48)
active^#(div(0,s(Y)))	→	mark^#(0)	(49)
if^#(X1,active(X2),X3)	→	if^#(X1,X2,X3)	(50)
mark^#(s(X))	→	s^#(mark(X))	(51)
mark^#(0)	→	active^#(0)	(52)
s^#(active(X))	→	s^#(X)	(53)
active^#(div(s(X),s(Y)))	→	div^#(minus(X,Y),s(Y))	(54)
active^#(div(s(X),s(Y)))	→	s^#(div(minus(X,Y),s(Y)))	(55)
active^#(geq(X,0))	→	mark^#(true)	(56)
mark^#(s(X))	→	active^#(s(mark(X)))	(57)
s^#(mark(X))	→	s^#(X)	(58)
mark^#(s(X))	→	mark^#(X)	(59)
div^#(mark(X1),X2)	→	div^#(X1,X2)	(60)
active^#(geq(0,s(Y)))	→	mark^#(false)	(61)
active^#(div(s(X),s(Y)))	→	minus^#(X,Y)	(62)
active^#(div(s(X),s(Y)))	→	mark^#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(63)
mark^#(geq(X1,X2))	→	active^#(geq(X1,X2))	(64)
geq^#(active(X1),X2)	→	geq^#(X1,X2)	(65)
geq^#(mark(X1),X2)	→	geq^#(X1,X2)	(66)
geq^#(X1,active(X2))	→	geq^#(X1,X2)	(67)
if^#(X1,X2,active(X3))	→	if^#(X1,X2,X3)	(68)
mark^#(div(X1,X2))	→	mark^#(X1)	(69)
active^#(geq(s(X),s(Y)))	→	mark^#(geq(X,Y))	(70)
active^#(div(s(X),s(Y)))	→	geq^#(X,Y)	(71)
mark^#(if(X1,X2,X3))	→	active^#(if(mark(X1),X2,X3))	(72)
if^#(X1,mark(X2),X3)	→	if^#(X1,X2,X3)	(73)
div^#(active(X1),X2)	→	div^#(X1,X2)	(74)
if^#(X1,X2,mark(X3))	→	if^#(X1,X2,X3)	(75)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(76)
mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
mark^#(if(X1,X2,X3))	→	mark^#(X1)	(78)
active^#(div(s(X),s(Y)))	→	if^#(geq(X,Y),s(div(minus(X,Y),s(Y))),0)	(79)
mark^#(true)	→	active^#(true)	(80)
div^#(X1,mark(X2))	→	div^#(X1,X2)	(81)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)
active^#(if(false,X,Y))	→	mark^#(Y)	(83)
div^#(X1,active(X2))	→	div^#(X1,X2)	(84)
if^#(active(X1),X2,X3)	→	if^#(X1,X2,X3)	(85)
minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(86)
geq^#(X1,mark(X2))	→	geq^#(X1,X2)	(87)

1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

The 1^st component contains the pair

mark^#(s(X))	→	mark^#(X)	(59)
mark^#(s(X))	→	active^#(s(mark(X)))	(57)
active^#(if(false,X,Y))	→	mark^#(Y)	(83)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)
mark^#(if(X1,X2,X3))	→	mark^#(X1)	(78)
mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
mark^#(if(X1,X2,X3))	→	active^#(if(mark(X1),X2,X3))	(72)
active^#(geq(s(X),s(Y)))	→	mark^#(geq(X,Y))	(70)
active^#(if(true,X,Y))	→	mark^#(X)	(46)
mark^#(div(X1,X2))	→	mark^#(X1)	(69)
mark^#(div(X1,X2))	→	active^#(div(mark(X1),X2))	(43)
mark^#(geq(X1,X2))	→	active^#(geq(X1,X2))	(64)
active^#(div(s(X),s(Y)))	→	mark^#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(63)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	0
[geq^#(x₁, x₂)]	=	0
[false]	=	0
[div(x₁, x₂)]	=	x₁ + x₂ + 21656
[geq(x₁, x₂)]	=	x₁ + 0
[true]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
active(geq(0,s(Y)))	→	mark(false)	(4)
mark(false)	→	active(false)	(15)
active(if(true,X,Y))	→	mark(X)	(8)
active(minus(0,Y))	→	mark(0)	(1)
active(geq(X,0))	→	mark(true)	(3)
mark(div(X1,X2))	→	active(div(mark(X1),X2))	(16)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
mark(if(X1,X2,X3))	→	active(if(mark(X1),X2,X3))	(17)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
active(geq(s(X),s(Y)))	→	mark(geq(X,Y))	(5)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
mark(minus(X1,X2))	→	active(minus(X1,X2))	(10)
active(div(s(X),s(Y)))	→	mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(7)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
mark(true)	→	active(true)	(14)
div(X1,active(X2))	→	div(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
mark(0)	→	active(0)	(11)
active(if(false,X,Y))	→	mark(Y)	(9)
mark(geq(X1,X2))	→	active(geq(X1,X2))	(13)
active(div(0,s(Y)))	→	mark(0)	(6)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(2)

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

mark^#(s(X))	→	mark^#(X)	(59)
active^#(geq(s(X),s(Y)))	→	mark^#(geq(X,Y))	(70)
mark^#(div(X1,X2))	→	mark^#(X1)	(69)

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

active^#(if(true,X,Y))	→	mark^#(X)	(46)
mark^#(div(X1,X2))	→	active^#(div(mark(X1),X2))	(43)
mark^#(if(X1,X2,X3))	→	mark^#(X1)	(78)
mark^#(if(X1,X2,X3))	→	active^#(if(mark(X1),X2,X3))	(72)
mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
active^#(div(s(X),s(Y)))	→	mark^#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(63)
mark^#(s(X))	→	active^#(s(mark(X)))	(57)
active^#(if(false,X,Y))	→	mark^#(Y)	(83)
mark^#(geq(X1,X2))	→	active^#(geq(X1,X2))	(64)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	12618
[minus(x₁, x₂)]	=	0
[geq^#(x₁, x₂)]	=	0
[false]	=	0
[div(x₁, x₂)]	=	x₂ + 23612
[geq(x₁, x₂)]	=	0
[true]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
active(geq(0,s(Y)))	→	mark(false)	(4)
mark(false)	→	active(false)	(15)
active(if(true,X,Y))	→	mark(X)	(8)
active(minus(0,Y))	→	mark(0)	(1)
active(geq(X,0))	→	mark(true)	(3)
mark(div(X1,X2))	→	active(div(mark(X1),X2))	(16)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
mark(if(X1,X2,X3))	→	active(if(mark(X1),X2,X3))	(17)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
active(geq(s(X),s(Y)))	→	mark(geq(X,Y))	(5)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
mark(minus(X1,X2))	→	active(minus(X1,X2))	(10)
active(div(s(X),s(Y)))	→	mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(7)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
mark(true)	→	active(true)	(14)
div(X1,active(X2))	→	div(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
mark(0)	→	active(0)	(11)
active(if(false,X,Y))	→	mark(Y)	(9)
mark(geq(X1,X2))	→	active(geq(X1,X2))	(13)
active(div(0,s(Y)))	→	mark(0)	(6)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(2)

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

active^#(div(s(X),s(Y)))

→

mark^#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))

(63)

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

active^#(if(true,X,Y))	→	mark^#(X)	(46)
mark^#(div(X1,X2))	→	active^#(div(mark(X1),X2))	(43)
mark^#(if(X1,X2,X3))	→	mark^#(X1)	(78)
mark^#(if(X1,X2,X3))	→	active^#(if(mark(X1),X2,X3))	(72)
mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
mark^#(s(X))	→	active^#(s(mark(X)))	(57)
active^#(if(false,X,Y))	→	mark^#(Y)	(83)
mark^#(geq(X1,X2))	→	active^#(geq(X1,X2))	(64)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	6960
[minus(x₁, x₂)]	=	7179
[geq^#(x₁, x₂)]	=	0
[false]	=	7177
[div(x₁, x₂)]	=	2332
[geq(x₁, x₂)]	=	584
[true]	=	7179
[mark^#(x₁)]	=	7179
[0]	=	7179
[if(x₁, x₂, x₃)]	=	7179
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	7179
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

mark^#(div(X1,X2))	→	active^#(div(mark(X1),X2))	(43)
mark^#(s(X))	→	active^#(s(mark(X)))	(57)
mark^#(geq(X1,X2))	→	active^#(geq(X1,X2))	(64)

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

active^#(if(true,X,Y))	→	mark^#(X)	(46)
mark^#(if(X1,X2,X3))	→	mark^#(X1)	(78)
mark^#(if(X1,X2,X3))	→	active^#(if(mark(X1),X2,X3))	(72)
mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
active^#(if(false,X,Y))	→	mark^#(Y)	(83)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	4187
[minus(x₁, x₂)]	=	27615
[geq^#(x₁, x₂)]	=	0
[false]	=	1
[div(x₁, x₂)]	=	50836
[geq(x₁, x₂)]	=	40691
[true]	=	23505
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	2805
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 3153
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 7179

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
active(geq(0,s(Y)))	→	mark(false)	(4)
mark(false)	→	active(false)	(15)
active(if(true,X,Y))	→	mark(X)	(8)
active(minus(0,Y))	→	mark(0)	(1)
active(geq(X,0))	→	mark(true)	(3)
mark(div(X1,X2))	→	active(div(mark(X1),X2))	(16)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
mark(if(X1,X2,X3))	→	active(if(mark(X1),X2,X3))	(17)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
active(geq(s(X),s(Y)))	→	mark(geq(X,Y))	(5)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
mark(minus(X1,X2))	→	active(minus(X1,X2))	(10)
active(div(s(X),s(Y)))	→	mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(7)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
mark(true)	→	active(true)	(14)
div(X1,active(X2))	→	div(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
mark(0)	→	active(0)	(11)
active(if(false,X,Y))	→	mark(Y)	(9)
mark(geq(X1,X2))	→	active(geq(X1,X2))	(13)
active(div(0,s(Y)))	→	mark(0)	(6)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(2)

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

active^#(if(true,X,Y))	→	mark^#(X)	(46)
mark^#(if(X1,X2,X3))	→	mark^#(X1)	(78)
active^#(if(false,X,Y))	→	mark^#(Y)	(83)

could be deleted.

1.1.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^#(if(X1,X2,X3))	→	active^#(if(mark(X1),X2,X3))	(72)
mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	15622
[minus(x₁, x₂)]	=	4
[geq^#(x₁, x₂)]	=	0
[false]	=	3
[div(x₁, x₂)]	=	1
[geq(x₁, x₂)]	=	3
[true]	=	23505
[mark^#(x₁)]	=	7179
[0]	=	3
[if(x₁, x₂, x₃)]	=	3
[s^#(x₁)]	=	0
[mark(x₁)]	=	2
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 7175

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

mark^#(if(X1,X2,X3))

→

active^#(if(mark(X1),X2,X3))

(72)

could be deleted.

1.1.1.1.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^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 5970
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	0
[false]	=	1
[div(x₁, x₂)]	=	x₁ + 35082
[geq(x₁, x₂)]	=	26051
[true]	=	19621
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
active(geq(0,s(Y)))	→	mark(false)	(4)
mark(false)	→	active(false)	(15)
active(if(true,X,Y))	→	mark(X)	(8)
active(minus(0,Y))	→	mark(0)	(1)
active(geq(X,0))	→	mark(true)	(3)
mark(div(X1,X2))	→	active(div(mark(X1),X2))	(16)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
mark(if(X1,X2,X3))	→	active(if(mark(X1),X2,X3))	(17)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
active(geq(s(X),s(Y)))	→	mark(geq(X,Y))	(5)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
mark(minus(X1,X2))	→	active(minus(X1,X2))	(10)
active(div(s(X),s(Y)))	→	mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(7)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
mark(true)	→	active(true)	(14)
div(X1,active(X2))	→	div(X1,X2)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
mark(0)	→	active(0)	(11)
active(if(false,X,Y))	→	mark(Y)	(9)
mark(geq(X1,X2))	→	active(geq(X1,X2))	(13)
active(div(0,s(Y)))	→	mark(0)	(6)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)
active(minus(s(X),s(Y)))	→	mark(minus(X,Y))	(2)

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

mark^#(minus(X1,X2))	→	active^#(minus(X1,X2))	(77)
active^#(minus(s(X),s(Y)))	→	mark^#(minus(X,Y))	(82)

could be deleted.

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

s^#(mark(X))	→	s^#(X)	(58)
s^#(active(X))	→	s^#(X)	(53)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	0
[false]	=	55977
[div(x₁, x₂)]	=	x₁ + 21310
[geq(x₁, x₂)]	=	55975
[true]	=	55977
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 2
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

s^#(mark(X))	→	s^#(X)	(58)
s^#(active(X))	→	s^#(X)	(53)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(86)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(76)
minus^#(X1,mark(X2))	→	minus^#(X1,X2)	(48)
minus^#(X1,active(X2))	→	minus^#(X1,X2)	(44)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	0
[false]	=	1771
[div(x₁, x₂)]	=	x₁ + 13068
[geq(x₁, x₂)]	=	1769
[true]	=	55977
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[active(x₁)]	=	x₁ + 2
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

minus^#(mark(X1),X2)	→	minus^#(X1,X2)	(86)
minus^#(active(X1),X2)	→	minus^#(X1,X2)	(76)
minus^#(X1,mark(X2))	→	minus^#(X1,X2)	(48)
minus^#(X1,active(X2))	→	minus^#(X1,X2)	(44)

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

geq^#(X1,mark(X2))	→	geq^#(X1,X2)	(87)
geq^#(X1,active(X2))	→	geq^#(X1,X2)	(67)
geq^#(mark(X1),X2)	→	geq^#(X1,X2)	(66)
geq^#(active(X1),X2)	→	geq^#(X1,X2)	(65)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	x₂ + 0
[false]	=	56025
[div(x₁, x₂)]	=	x₁ + 45071
[geq(x₁, x₂)]	=	56023
[true]	=	56025
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 2
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

geq^#(X1,mark(X2))	→	geq^#(X1,X2)	(87)
geq^#(X1,active(X2))	→	geq^#(X1,X2)	(67)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

geq^#(active(X1),X2)	→	geq^#(X1,X2)	(65)
geq^#(mark(X1),X2)	→	geq^#(X1,X2)	(66)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	x₁ + 0
[false]	=	1065
[div(x₁, x₂)]	=	x₁ + 32688
[geq(x₁, x₂)]	=	1063
[true]	=	1065
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 2
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

geq^#(active(X1),X2)	→	geq^#(X1,X2)	(65)
geq^#(mark(X1),X2)	→	geq^#(X1,X2)	(66)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

if^#(active(X1),X2,X3)	→	if^#(X1,X2,X3)	(85)
if^#(X1,X2,mark(X3))	→	if^#(X1,X2,X3)	(75)
if^#(X1,active(X2),X3)	→	if^#(X1,X2,X3)	(50)
if^#(X1,mark(X2),X3)	→	if^#(X1,X2,X3)	(73)
if^#(X1,X2,active(X3))	→	if^#(X1,X2,X3)	(68)
if^#(mark(X1),X2,X3)	→	if^#(X1,X2,X3)	(45)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	0
[false]	=	1065
[div(x₁, x₂)]	=	x₁ + 11297
[geq(x₁, x₂)]	=	1
[true]	=	1065
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 2
[if^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

if^#(X1,X2,mark(X3))	→	if^#(X1,X2,X3)	(75)
if^#(X1,active(X2),X3)	→	if^#(X1,X2,X3)	(50)
if^#(X1,mark(X2),X3)	→	if^#(X1,X2,X3)	(73)
if^#(X1,X2,active(X3))	→	if^#(X1,X2,X3)	(68)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

if^#(mark(X1),X2,X3)	→	if^#(X1,X2,X3)	(45)
if^#(active(X1),X2,X3)	→	if^#(X1,X2,X3)	(85)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	0
[false]	=	435
[div(x₁, x₂)]	=	x₁ + 1
[geq(x₁, x₂)]	=	433
[true]	=	1065
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 8573
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 8574
[if^#(x₁, x₂, x₃)]	=	x₁ + 0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

if^#(mark(X1),X2,X3)	→	if^#(X1,X2,X3)	(45)
if^#(active(X1),X2,X3)	→	if^#(X1,X2,X3)	(85)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

div^#(mark(X1),X2)	→	div^#(X1,X2)	(60)
div^#(X1,active(X2))	→	div^#(X1,X2)	(84)
div^#(X1,mark(X2))	→	div^#(X1,X2)	(81)
div^#(active(X1),X2)	→	div^#(X1,X2)	(74)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	x₁ + x₂ + 0
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	0
[false]	=	8327
[div(x₁, x₂)]	=	x₁ + 1
[geq(x₁, x₂)]	=	1
[true]	=	32301
[mark^#(x₁)]	=	x₁ + 7179
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 249
[minus^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 8574
[if^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	7178

together with the usable rules

minus(mark(X1),X2)	→	minus(X1,X2)	(18)
minus(X1,active(X2))	→	minus(X1,X2)	(21)
if(X1,active(X2),X3)	→	if(X1,X2,X3)	(36)
geq(active(X1),X2)	→	geq(X1,X2)	(26)
minus(X1,mark(X2))	→	minus(X1,X2)	(19)
if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(32)
geq(X1,active(X2))	→	geq(X1,X2)	(27)
if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(22)
div(mark(X1),X2)	→	div(X1,X2)	(28)
if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(33)
minus(active(X1),X2)	→	minus(X1,X2)	(20)
geq(X1,mark(X2))	→	geq(X1,X2)	(25)
div(active(X1),X2)	→	div(X1,X2)	(30)
div(X1,active(X2))	→	div(X1,X2)	(31)
s(active(X))	→	s(X)	(23)
geq(mark(X1),X2)	→	geq(X1,X2)	(24)
if(X1,X2,active(X3))	→	if(X1,X2,X3)	(37)
if(active(X1),X2,X3)	→	if(X1,X2,X3)	(35)
div(X1,mark(X2))	→	div(X1,X2)	(29)

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

div^#(mark(X1),X2)	→	div^#(X1,X2)	(60)
div^#(X1,active(X2))	→	div^#(X1,X2)	(84)
div^#(X1,mark(X2))	→	div^#(X1,X2)	(81)
div^#(active(X1),X2)	→	div^#(X1,X2)	(74)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.