Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci02)

The rewrite relation of the following TRS is considered.

p(0)	→	0	(1)
p(s(x))	→	x	(2)
plus(x,0)	→	x	(3)
plus(0,y)	→	y	(4)
plus(s(x),y)	→	s(plus(x,y))	(5)
plus(s(x),y)	→	s(plus(p(s(x)),y))	(6)
plus(x,s(y))	→	s(plus(x,p(s(y))))	(7)
times(0,y)	→	0	(8)
times(s(0),y)	→	y	(9)
times(s(x),y)	→	plus(y,times(x,y))	(10)
div(0,y)	→	0	(11)
div(x,y)	→	quot(x,y,y)	(12)
quot(zero(y),s(y),z)	→	0	(13)
quot(s(x),s(y),z)	→	quot(x,y,z)	(14)
quot(x,0,s(z))	→	s(div(x,s(z)))	(15)
div(div(x,y),z)	→	div(x,times(zero(y),z))	(16)
eq(0,0)	→	true	(17)
eq(s(x),0)	→	false	(18)
eq(0,s(y))	→	false	(19)
eq(s(x),s(y))	→	eq(x,y)	(20)
divides(y,x)	→	eq(x,times(div(x,y),y))	(21)
prime(s(s(x)))	→	pr(s(s(x)),s(x))	(22)
pr(x,s(0))	→	true	(23)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(24)
if(true,x,y)	→	false	(25)
if(false,x,y)	→	pr(x,y)	(26)
zero(div(x,x))	→	x	(27)
zero(divides(x,x))	→	x	(28)
zero(times(x,x))	→	x	(29)
zero(quot(x,x,x))	→	x	(30)
zero(s(x))	→	if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(31)

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.

plus^#(s(x),y)	→	p^#(s(x))	(32)
zero^#(s(x))	→	if^#(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(33)
eq^#(s(x),s(y))	→	eq^#(x,y)	(34)
zero^#(s(x))	→	zero^#(0)	(35)
zero^#(s(x))	→	zero^#(0)	(35)
div^#(div(x,y),z)	→	div^#(x,times(zero(y),z))	(36)
divides^#(y,x)	→	div^#(x,y)	(37)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(38)
plus^#(x,s(y))	→	plus^#(x,p(s(y)))	(39)
div^#(div(x,y),z)	→	times^#(zero(y),z)	(40)
if^#(false,x,y)	→	pr^#(x,y)	(41)
zero^#(s(x))	→	eq^#(x,s(0))	(42)
zero^#(s(x))	→	plus^#(0,zero(0))	(43)
div^#(x,y)	→	quot^#(x,y,y)	(44)
divides^#(y,x)	→	times^#(div(x,y),y)	(45)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(46)
times^#(s(x),y)	→	times^#(x,y)	(47)
prime^#(s(s(x)))	→	pr^#(s(s(x)),s(x))	(48)
div^#(div(x,y),z)	→	zero^#(y)	(49)
divides^#(y,x)	→	eq^#(x,times(div(x,y),y))	(50)
times^#(s(x),y)	→	plus^#(y,times(x,y))	(51)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(52)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(53)
zero^#(s(x))	→	plus^#(zero(0),0)	(54)
plus^#(x,s(y))	→	p^#(s(y))	(55)
pr^#(x,s(s(y)))	→	divides^#(s(s(y)),x)	(56)
plus^#(s(x),y)	→	plus^#(x,y)	(57)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

pr^#(x,s(s(y)))	→	divides^#(s(s(y)),x)	(56)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(38)
divides^#(y,x)	→	div^#(x,y)	(37)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(52)
div^#(div(x,y),z)	→	div^#(x,times(zero(y),z))	(36)
div^#(div(x,y),z)	→	zero^#(y)	(49)
zero^#(s(x))	→	if^#(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(33)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(46)
div^#(x,y)	→	quot^#(x,y,y)	(44)
if^#(false,x,y)	→	pr^#(x,y)	(41)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	x₁ + 2
[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	x₁ + 2
[eq(x₁, x₂)]	=	x₂ + 0
[false]	=	2
[div(x₁, x₂)]	=	x₁ + x₂ + 9515
[p^#(x₁)]	=	0
[true]	=	2
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	2
[quot(x₁, x₂, x₃)]	=	x₃ + 9516
[times(x₁, x₂)]	=	x₁ + 9514
[pr(x₁, x₂)]	=	2
[divides^#(x₁, x₂)]	=	x₂ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 9507
[if^#(x₁, x₂, x₃)]	=	x₂ + 2
[quot^#(x₁, x₂, x₃)]	=	x₁ + 0
[zero^#(x₁)]	=	x₁ + 9514
[divides(x₁, x₂)]	=	x₂ + 1673

together with the usable rules

plus(0,y)	→	y	(4)
p(0)	→	0	(1)
plus(x,0)	→	x	(3)
if(false,x,y)	→	pr(x,y)	(26)
zero(div(x,x))	→	x	(27)
zero(divides(x,x))	→	x	(28)
plus(s(x),y)	→	s(plus(x,y))	(5)
plus(x,s(y))	→	s(plus(x,p(s(y))))	(7)
if(true,x,y)	→	false	(25)
zero(quot(x,x,x))	→	x	(30)
zero(s(x))	→	if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(31)
pr(x,s(0))	→	true	(23)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(24)
plus(s(x),y)	→	s(plus(p(s(x)),y))	(6)
zero(times(x,x))	→	x	(29)
p(s(x))	→	x	(2)

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

pr^#(x,s(s(y)))	→	divides^#(s(s(y)),x)	(56)
divides^#(y,x)	→	div^#(x,y)	(37)
div^#(div(x,y),z)	→	div^#(x,times(zero(y),z))	(36)
div^#(div(x,y),z)	→	zero^#(y)	(49)
zero^#(s(x))	→	if^#(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(33)

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

quot^#(x,0,s(z))	→	div^#(x,s(z))	(46)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(38)
div^#(x,y)	→	quot^#(x,y,y)	(44)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	x₁ + 1
[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	2
[eq(x₁, x₂)]	=	x₂ + 0
[false]	=	2
[div(x₁, x₂)]	=	x₁ + x₂ + 1
[p^#(x₁)]	=	0
[true]	=	2
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	0
[times^#(x₁, x₂)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	2
[quot(x₁, x₂, x₃)]	=	x₃ + 9516
[times(x₁, x₂)]	=	x₁ + x₂ + 1
[pr(x₁, x₂)]	=	2
[divides^#(x₁, x₂)]	=	1
[plus(x₁, x₂)]	=	x₁ + 15945
[if^#(x₁, x₂, x₃)]	=	2
[quot^#(x₁, x₂, x₃)]	=	x₁ + 0
[zero^#(x₁)]	=	9514
[divides(x₁, x₂)]	=	x₂ + 1

together with the usable rules

plus(x,0)	→	x	(3)
if(false,x,y)	→	pr(x,y)	(26)
zero(div(x,x))	→	x	(27)
zero(divides(x,x))	→	x	(28)
if(true,x,y)	→	false	(25)
zero(quot(x,x,x))	→	x	(30)
zero(s(x))	→	if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(31)
pr(x,s(0))	→	true	(23)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(24)
zero(times(x,x))	→	x	(29)

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

quot^#(s(x),s(y),z)

→

quot^#(x,y,z)

(38)

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

quot^#(x,0,s(z))	→	div^#(x,s(z))	(46)
div^#(x,y)	→	quot^#(x,y,y)	(44)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	0
[div^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[s(x₁)]	=	0
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	max(0)
[pr^#(x₁, x₂)]	=	max(0)
[eq(x₁, x₂)]	=	max(0)
[false]	=	0
[div(x₁, x₂)]	=	max(0)
[p^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	max(0)
[prime^#(x₁)]	=	0
[p(x₁)]	=	0
[times^#(x₁, x₂)]	=	max(0)
[0]	=	3
[if(x₁, x₂, x₃)]	=	max(0)
[quot(x₁, x₂, x₃)]	=	max(0)
[times(x₁, x₂)]	=	max(0)
[pr(x₁, x₂)]	=	max(0)
[divides^#(x₁, x₂)]	=	max(0)
[plus(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[quot^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 1, 0)
[zero^#(x₁)]	=	0
[divides(x₁, x₂)]	=	max(0)

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

quot^#(x,0,s(z))	→	div^#(x,s(z))	(46)
div^#(x,y)	→	quot^#(x,y,y)	(44)

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

if^#(false,x,y)	→	pr^#(x,y)	(41)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(52)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	x₁ + 0
[div^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 845
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	max(0)
[pr^#(x₁, x₂)]	=	max(x₂ + 3, 0)
[eq(x₁, x₂)]	=	max(0)
[false]	=	0
[div(x₁, x₂)]	=	max(x₁ + 847, 0)
[p^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	max(0)
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	max(0)
[0]	=	849
[if(x₁, x₂, x₃)]	=	max(x₁ + 846, x₂ + 848, x₃ + 1437, 0)
[quot(x₁, x₂, x₃)]	=	max(x₁ + 848, x₂ + 2, x₃ + 1, 0)
[times(x₁, x₂)]	=	max(x₁ + 35495, x₂ + 1, 0)
[pr(x₁, x₂)]	=	max(x₁ + 847, 0)
[divides^#(x₁, x₂)]	=	max(0)
[plus(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(x₁ + 1, x₃ + 4, 0)
[quot^#(x₁, x₂, x₃)]	=	max(0)
[zero^#(x₁)]	=	0
[divides(x₁, x₂)]	=	max(x₁ + 1, 0)

together with the usable rules

eq(s(x),0)	→	false	(18)
divides(y,x)	→	eq(x,times(div(x,y),y))	(21)
eq(0,s(y))	→	false	(19)
eq(0,0)	→	true	(17)
eq(s(x),s(y))	→	eq(x,y)	(20)

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

if^#(false,x,y)	→	pr^#(x,y)	(41)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(52)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

times^#(s(x),y)

→

times^#(x,y)

(47)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	x₁ + 12
[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	1
[eq(x₁, x₂)]	=	x₁ + x₂ + 5
[false]	=	9
[div(x₁, x₂)]	=	x₁ + x₂ + 0
[p^#(x₁)]	=	0
[true]	=	10
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	1
[times^#(x₁, x₂)]	=	x₁ + 0
[0]	=	2
[if(x₁, x₂, x₃)]	=	13
[quot(x₁, x₂, x₃)]	=	x₃ + 9517
[times(x₁, x₂)]	=	x₁ + 1
[pr(x₁, x₂)]	=	13
[divides^#(x₁, x₂)]	=	1
[plus(x₁, x₂)]	=	26729
[if^#(x₁, x₂, x₃)]	=	0
[quot^#(x₁, x₂, x₃)]	=	0
[zero^#(x₁)]	=	9514
[divides(x₁, x₂)]	=	x₂ + 2

together with the usable rules

if(false,x,y)	→	pr(x,y)	(26)
zero(div(x,x))	→	x	(27)
zero(divides(x,x))	→	x	(28)
if(true,x,y)	→	false	(25)
zero(quot(x,x,x))	→	x	(30)
zero(s(x))	→	if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(31)
pr(x,s(0))	→	true	(23)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(24)
zero(times(x,x))	→	x	(29)

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

times^#(s(x),y)

→

times^#(x,y)

(47)

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

plus^#(s(x),y)	→	plus^#(x,y)	(57)
plus^#(x,s(y))	→	plus^#(x,p(s(y)))	(39)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(53)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	x₁ + 12
[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	x₁ + 0
[pr^#(x₁, x₂)]	=	1
[eq(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	9
[div(x₁, x₂)]	=	x₁ + x₂ + 0
[p^#(x₁)]	=	0
[true]	=	3
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	13
[quot(x₁, x₂, x₃)]	=	x₃ + 1
[times(x₁, x₂)]	=	x₁ + 29639
[pr(x₁, x₂)]	=	13
[divides^#(x₁, x₂)]	=	1
[plus(x₁, x₂)]	=	29641
[if^#(x₁, x₂, x₃)]	=	0
[quot^#(x₁, x₂, x₃)]	=	0
[zero^#(x₁)]	=	9514
[divides(x₁, x₂)]	=	x₂ + 11495

together with the usable rules

p(0)	→	0	(1)
if(false,x,y)	→	pr(x,y)	(26)
zero(div(x,x))	→	x	(27)
zero(divides(x,x))	→	x	(28)
if(true,x,y)	→	false	(25)
zero(quot(x,x,x))	→	x	(30)
zero(s(x))	→	if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(31)
pr(x,s(0))	→	true	(23)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(24)
zero(times(x,x))	→	x	(29)
p(s(x))	→	x	(2)

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

plus^#(s(x),y)

→

plus^#(x,y)

(57)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(x,s(y))	→	plus^#(x,p(s(y)))	(39)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(53)

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(div^#)	=	2
π(pr^#)	=	1

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

prec(zero)	=	0	status(zero)	=	[]	list-extension(zero)	=	Lex
prec(s)	=	1	status(s)	=	[]	list-extension(s)	=	Lex
prec(prime)	=	0	status(prime)	=	[]	list-extension(prime)	=	Lex
prec(plus^#)	=	0	status(plus^#)	=	[2]	list-extension(plus^#)	=	Lex
prec(eq)	=	0	status(eq)	=	[2, 1]	list-extension(eq)	=	Lex
prec(false)	=	0	status(false)	=	[]	list-extension(false)	=	Lex
prec(div)	=	0	status(div)	=	[1, 2]	list-extension(div)	=	Lex
prec(p^#)	=	0	status(p^#)	=	[]	list-extension(p^#)	=	Lex
prec(true)	=	0	status(true)	=	[]	list-extension(true)	=	Lex
prec(eq^#)	=	0	status(eq^#)	=	[1, 2]	list-extension(eq^#)	=	Lex
prec(prime^#)	=	0	status(prime^#)	=	[]	list-extension(prime^#)	=	Lex
prec(p)	=	0	status(p)	=	[]	list-extension(p)	=	Lex
prec(times^#)	=	0	status(times^#)	=	[]	list-extension(times^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(if)	=	0	status(if)	=	[3, 2, 1]	list-extension(if)	=	Lex
prec(quot)	=	0	status(quot)	=	[2, 1, 3]	list-extension(quot)	=	Lex
prec(times)	=	0	status(times)	=	[1, 2]	list-extension(times)	=	Lex
prec(pr)	=	0	status(pr)	=	[1, 2]	list-extension(pr)	=	Lex
prec(divides^#)	=	0	status(divides^#)	=	[]	list-extension(divides^#)	=	Lex
prec(plus)	=	0	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(if^#)	=	0	status(if^#)	=	[3, 2, 1]	list-extension(if^#)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[3, 2, 1]	list-extension(quot^#)	=	Lex
prec(zero^#)	=	0	status(zero^#)	=	[]	list-extension(zero^#)	=	Lex
prec(divides)	=	0	status(divides)	=	[1, 2]	list-extension(divides)	=	Lex

and the following Max-polynomial interpretation

[zero(x₁)]	=	1
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	1
[plus^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[eq(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[false]	=	0
[div(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[p^#(x₁)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[prime^#(x₁)]	=	1
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[0]	=	7758
[if(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[quot(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[times(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[pr(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[divides^#(x₁, x₂)]	=	x₂ + 1
[plus(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[if^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[quot^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[zero^#(x₁)]	=	1
[divides(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)

together with the usable rules

p(0)	→	0	(1)
p(s(x))	→	x	(2)

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

plus^#(x,s(y))

→

plus^#(x,p(s(y)))

(39)

could be deleted.

1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(s(x),y)

→

plus^#(p(s(x)),y)

(53)

1.1.3.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(div^#)	=	2
π(pr^#)	=	1

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

prec(zero)	=	0	status(zero)	=	[]	list-extension(zero)	=	Lex
prec(s)	=	1	status(s)	=	[]	list-extension(s)	=	Lex
prec(prime)	=	0	status(prime)	=	[]	list-extension(prime)	=	Lex
prec(plus^#)	=	2	status(plus^#)	=	[2, 1]	list-extension(plus^#)	=	Lex
prec(eq)	=	0	status(eq)	=	[2, 1]	list-extension(eq)	=	Lex
prec(false)	=	0	status(false)	=	[]	list-extension(false)	=	Lex
prec(div)	=	0	status(div)	=	[1, 2]	list-extension(div)	=	Lex
prec(p^#)	=	0	status(p^#)	=	[]	list-extension(p^#)	=	Lex
prec(true)	=	0	status(true)	=	[]	list-extension(true)	=	Lex
prec(eq^#)	=	0	status(eq^#)	=	[1, 2]	list-extension(eq^#)	=	Lex
prec(prime^#)	=	0	status(prime^#)	=	[]	list-extension(prime^#)	=	Lex
prec(p)	=	0	status(p)	=	[]	list-extension(p)	=	Lex
prec(times^#)	=	0	status(times^#)	=	[]	list-extension(times^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(if)	=	0	status(if)	=	[3, 2, 1]	list-extension(if)	=	Lex
prec(quot)	=	0	status(quot)	=	[2, 1, 3]	list-extension(quot)	=	Lex
prec(times)	=	0	status(times)	=	[1, 2]	list-extension(times)	=	Lex
prec(pr)	=	0	status(pr)	=	[1, 2]	list-extension(pr)	=	Lex
prec(divides^#)	=	0	status(divides^#)	=	[]	list-extension(divides^#)	=	Lex
prec(plus)	=	0	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(if^#)	=	0	status(if^#)	=	[3, 2, 1]	list-extension(if^#)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[3, 2, 1]	list-extension(quot^#)	=	Lex
prec(zero^#)	=	0	status(zero^#)	=	[]	list-extension(zero^#)	=	Lex
prec(divides)	=	0	status(divides)	=	[1, 2]	list-extension(divides)	=	Lex

and the following Max-polynomial interpretation

[zero(x₁)]	=	1
[s(x₁)]	=	x₁ + 2
[prime(x₁)]	=	1
[plus^#(x₁, x₂)]	=	max(x₁ + 21239, x₂ + 1, 0)
[eq(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[false]	=	0
[div(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[p^#(x₁)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[prime^#(x₁)]	=	1
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[0]	=	7758
[if(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[quot(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[times(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[pr(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[divides^#(x₁, x₂)]	=	x₂ + 1
[plus(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[if^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[quot^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[zero^#(x₁)]	=	1
[divides(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)

together with the usable rules

p(0)	→	0	(1)
p(s(x))	→	x	(2)

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

plus^#(s(x),y)

→

plus^#(p(s(x)),y)

(53)

could be deleted.

1.1.3.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

eq^#(s(x),s(y))

→

eq^#(x,y)

(34)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero(x₁)]	=	x₁ + 12
[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	1
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	9
[div(x₁, x₂)]	=	x₁ + x₂ + 0
[p^#(x₁)]	=	0
[true]	=	6
[eq^#(x₁, x₂)]	=	x₁ + 0
[prime^#(x₁)]	=	0
[p(x₁)]	=	1
[times^#(x₁, x₂)]	=	0
[0]	=	2
[if(x₁, x₂, x₃)]	=	13
[quot(x₁, x₂, x₃)]	=	x₃ + 2
[times(x₁, x₂)]	=	x₁ + 1
[pr(x₁, x₂)]	=	13
[divides^#(x₁, x₂)]	=	1
[plus(x₁, x₂)]	=	722
[if^#(x₁, x₂, x₃)]	=	0
[quot^#(x₁, x₂, x₃)]	=	0
[zero^#(x₁)]	=	9514
[divides(x₁, x₂)]	=	x₂ + 1

together with the usable rules

if(false,x,y)	→	pr(x,y)	(26)
zero(div(x,x))	→	x	(27)
zero(divides(x,x))	→	x	(28)
if(true,x,y)	→	false	(25)
zero(quot(x,x,x))	→	x	(30)
zero(s(x))	→	if(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0))))	(31)
pr(x,s(0))	→	true	(23)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(24)
zero(times(x,x))	→	x	(29)

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

eq^#(s(x),s(y))

→

eq^#(x,y)

(34)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.