Certification Problem

Input (TPDB TRS_Standard/AProVE_04/IJCAR_18)

The rewrite relation of the following TRS is considered.

plus(x,0)	→	x	(1)
plus(0,y)	→	y	(2)
plus(s(x),y)	→	s(plus(x,y))	(3)
times(0,y)	→	0	(4)
times(s(0),y)	→	y	(5)
times(s(x),y)	→	plus(y,times(x,y))	(6)
div(0,y)	→	0	(7)
div(x,y)	→	quot(x,y,y)	(8)
quot(0,s(y),z)	→	0	(9)
quot(s(x),s(y),z)	→	quot(x,y,z)	(10)
quot(x,0,s(z))	→	s(div(x,s(z)))	(11)
div(div(x,y),z)	→	div(x,times(y,z))	(12)
eq(0,0)	→	true	(13)
eq(s(x),0)	→	false	(14)
eq(0,s(y))	→	false	(15)
eq(s(x),s(y))	→	eq(x,y)	(16)
divides(y,x)	→	eq(x,times(div(x,y),y))	(17)
prime(s(s(x)))	→	pr(s(s(x)),s(x))	(18)
pr(x,s(0))	→	true	(19)
pr(x,s(s(y)))	→	if(divides(s(s(y)),x),x,s(y))	(20)
if(true,x,y)	→	false	(21)
if(false,x,y)	→	pr(x,y)	(22)

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.

times^#(s(x),y)	→	times^#(x,y)	(23)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(24)
eq^#(s(x),s(y))	→	eq^#(x,y)	(25)
if^#(false,x,y)	→	pr^#(x,y)	(26)
divides^#(y,x)	→	times^#(div(x,y),y)	(27)
divides^#(y,x)	→	div^#(x,y)	(28)
plus^#(s(x),y)	→	plus^#(x,y)	(29)
pr^#(x,s(s(y)))	→	divides^#(s(s(y)),x)	(30)
divides^#(y,x)	→	eq^#(x,times(div(x,y),y))	(31)
div^#(div(x,y),z)	→	times^#(y,z)	(32)
prime^#(s(s(x)))	→	pr^#(s(s(x)),s(x))	(33)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(34)
times^#(s(x),y)	→	plus^#(y,times(x,y))	(35)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(36)
div^#(x,y)	→	quot^#(x,y,y)	(37)
div^#(div(x,y),z)	→	div^#(x,times(y,z))	(38)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

if^#(false,x,y)	→	pr^#(x,y)	(26)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(24)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

eq(0,s(y))	→	false	(15)
eq(s(x),s(y))	→	eq(x,y)	(16)
eq(s(x),0)	→	false	(14)
eq(0,0)	→	true	(13)

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

if^#(false,x,y)	→	pr^#(x,y)	(26)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(24)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

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

→

eq^#(x,y)

(25)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 26287
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	0
[div(x₁, x₂)]	=	x₂ + 52572
[true]	=	0
[eq^#(x₁, x₂)]	=	x₁ + x₂ + 0
[prime^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	0
[0]	=	52573
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₂ + x₃ + 26285
[times(x₁, x₂)]	=	x₁ + 1
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + 26289
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	x₂ + 52573

together with the usable rules

eq(0,s(y))	→	false	(15)
eq(s(x),s(y))	→	eq(x,y)	(16)
eq(s(x),0)	→	false	(14)
eq(0,0)	→	true	(13)

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

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

→

eq^#(x,y)

(25)

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

div^#(div(x,y),z)	→	div^#(x,times(y,z))	(38)
div^#(x,y)	→	quot^#(x,y,y)	(37)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(36)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(34)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	0
[div(x₁, x₂)]	=	x₁ + x₂ + 9727
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	0
[0]	=	9727
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[times(x₁, x₂)]	=	9728
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + 9729
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	x₁ + 0
[divides(x₁, x₂)]	=	x₂ + 9728

together with the usable rules

eq(0,s(y))	→	false	(15)
eq(s(x),s(y))	→	eq(x,y)	(16)
eq(s(x),0)	→	false	(14)
eq(0,0)	→	true	(13)

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

div^#(div(x,y),z)	→	div^#(x,times(y,z))	(38)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(36)

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

div^#(x,y)	→	quot^#(x,y,y)	(37)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(34)

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	max(x₂ + 21240, 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)
[true]	=	0
[eq^#(x₁, x₂)]	=	max(0)
[prime^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	max(0)
[0]	=	21239
[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₂ + 1, 0)
[divides(x₁, x₂)]	=	max(0)

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

div^#(x,y)

→

quot^#(x,y,y)

(37)

could be deleted.

1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

times^#(s(x),y)

→

times^#(x,y)

(23)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

eq(0,s(y))	→	false	(15)
eq(s(x),s(y))	→	eq(x,y)	(16)
eq(s(x),0)	→	false	(14)
eq(0,0)	→	true	(13)

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

times^#(s(x),y)

→

times^#(x,y)

(23)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

plus^#(s(x),y)

→

plus^#(x,y)

(29)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

eq(0,s(y))	→	false	(15)
eq(s(x),s(y))	→	eq(x,y)	(16)
eq(s(x),0)	→	false	(14)
eq(0,0)	→	true	(13)

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

plus^#(s(x),y)

→

plus^#(x,y)

(29)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.