Certification Problem

Input (TPDB TRS_Standard/AProVE_04/IJCAR_26a)

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(0,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(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)

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))	(27)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(28)
prime^#(s(s(x)))	→	pr^#(s(s(x)),s(x))	(29)
plus^#(x,s(y))	→	p^#(s(y))	(30)
times^#(s(x),y)	→	times^#(x,y)	(31)
plus^#(s(x),y)	→	plus^#(x,y)	(32)
if^#(false,x,y)	→	pr^#(x,y)	(33)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(34)
eq^#(s(x),s(y))	→	eq^#(x,y)	(35)
times^#(s(x),y)	→	plus^#(y,times(x,y))	(36)
div^#(x,y)	→	quot^#(x,y,y)	(37)
divides^#(y,x)	→	div^#(x,y)	(38)
div^#(div(x,y),z)	→	times^#(y,z)	(39)
divides^#(y,x)	→	times^#(div(x,y),y)	(40)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(41)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(42)
plus^#(x,s(y))	→	plus^#(x,p(s(y)))	(43)
divides^#(y,x)	→	eq^#(x,times(div(x,y),y))	(44)
pr^#(x,s(s(y)))	→	divides^#(s(s(y)),x)	(45)
div^#(div(x,y),z)	→	div^#(x,times(y,z))	(46)

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)	(33)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(41)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 9727
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	9732
[div(x₁, x₂)]	=	x₁ + 1
[p^#(x₁)]	=	0
[true]	=	8
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 2240
[times^#(x₁, x₂)]	=	0
[0]	=	3
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₃ + 2
[times(x₁, x₂)]	=	x₁ + x₂ + 47339
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₂ + 11051
[if^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	47340

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

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

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)

(35)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	33860
[div(x₁, x₂)]	=	x₁ + 33855
[p^#(x₁)]	=	0
[true]	=	67716
[eq^#(x₁, x₂)]	=	x₁ + 0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 11966
[times^#(x₁, x₂)]	=	0
[0]	=	33857
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₃ + 33856
[times(x₁, x₂)]	=	x₁ + x₂ + 23612
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₂ + 11051
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	57467

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

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

→

eq^#(x,y)

(35)

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))	(46)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(28)
div^#(x,y)	→	quot^#(x,y,y)	(37)
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₂ + 1
[false]	=	6
[div(x₁, x₂)]	=	x₁ + 1
[p^#(x₁)]	=	0
[true]	=	8
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 7578
[times^#(x₁, x₂)]	=	0
[0]	=	3
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₃ + 2
[times(x₁, x₂)]	=	x₁ + x₂ + 43324
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₂ + 17068
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	x₁ + 0
[divides(x₁, x₂)]	=	43325

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

div^#(div(x,y),z)	→	div^#(x,times(y,z))	(46)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(28)

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

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

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

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

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

→

div^#(x,s(z))

(34)

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)

(31)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	36723
[div(x₁, x₂)]	=	x₁ + 36718
[p^#(x₁)]	=	0
[true]	=	73442
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 7578
[times^#(x₁, x₂)]	=	x₁ + 0
[0]	=	36720
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₃ + 36719
[times(x₁, x₂)]	=	x₁ + 1
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	11652
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	36719

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

times^#(s(x),y)

→

times^#(x,y)

(31)

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)	(32)
plus^#(x,s(y))	→	plus^#(x,p(s(y)))	(43)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(42)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	x₁ + 0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	28036
[div(x₁, x₂)]	=	x₁ + 28031
[p^#(x₁)]	=	0
[true]	=	56068
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	0
[0]	=	28033
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₃ + 28032
[times(x₁, x₂)]	=	x₁ + 1
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	33304
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	28032

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^#(x,y)

(32)

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

plus^#(x,s(y))	→	plus^#(x,p(s(y)))	(43)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(42)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(plus^#)	=	1
π(times^#)	=	1
π(if)	=	3

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

prec(div^#)	=	0	status(div^#)	=	[2]	list-extension(div^#)	=	Lex
prec(s)	=	1	status(s)	=	[]	list-extension(s)	=	Lex
prec(prime)	=	0	status(prime)	=	[]	list-extension(prime)	=	Lex
prec(pr^#)	=	0	status(pr^#)	=	[2, 1]	list-extension(pr^#)	=	Lex
prec(eq)	=	0	status(eq)	=	[2]	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^#)	=	[]	list-extension(eq^#)	=	Lex
prec(prime^#)	=	0	status(prime^#)	=	[]	list-extension(prime^#)	=	Lex
prec(p)	=	0	status(p)	=	[]	list-extension(p)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	0	status(quot)	=	[3, 2, 1]	list-extension(quot)	=	Lex
prec(times)	=	0	status(times)	=	[2, 1]	list-extension(times)	=	Lex
prec(pr)	=	0	status(pr)	=	[1]	list-extension(pr)	=	Lex
prec(divides^#)	=	0	status(divides^#)	=	[1, 2]	list-extension(divides^#)	=	Lex
prec(plus)	=	0	status(plus)	=	[]	list-extension(plus)	=	Lex
prec(if^#)	=	0	status(if^#)	=	[1, 2, 3]	list-extension(if^#)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[3, 2, 1]	list-extension(quot^#)	=	Lex
prec(divides)	=	0	status(divides)	=	[1, 2]	list-extension(divides)	=	Lex

and the following Max-polynomial interpretation

[div^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	1
[pr^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[eq(x₁, x₂)]	=	max(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, 0)
[prime^#(x₁)]	=	1
[p(x₁)]	=	x₁ + 0
[0]	=	23676
[quot(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[times(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[pr(x₁, x₂)]	=	x₁ + 1
[divides^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[plus(x₁, x₂)]	=	max(x₂ + 1, 0)
[if^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[quot^#(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[divides(x₁, x₂)]	=	x₁ + x₂ + 1

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)

(42)

could be deleted.

1.1.5.1.1.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)))

(43)

1.1.5.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(plus^#)	=	2
π(times^#)	=	1
π(if)	=	3

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

prec(div^#)	=	0	status(div^#)	=	[2]	list-extension(div^#)	=	Lex
prec(s)	=	2	status(s)	=	[]	list-extension(s)	=	Lex
prec(prime)	=	0	status(prime)	=	[]	list-extension(prime)	=	Lex
prec(pr^#)	=	0	status(pr^#)	=	[2, 1]	list-extension(pr^#)	=	Lex
prec(eq)	=	0	status(eq)	=	[2]	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^#)	=	[]	list-extension(eq^#)	=	Lex
prec(prime^#)	=	0	status(prime^#)	=	[]	list-extension(prime^#)	=	Lex
prec(p)	=	1	status(p)	=	[]	list-extension(p)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	0	status(quot)	=	[3, 2, 1]	list-extension(quot)	=	Lex
prec(times)	=	0	status(times)	=	[2, 1]	list-extension(times)	=	Lex
prec(pr)	=	0	status(pr)	=	[1]	list-extension(pr)	=	Lex
prec(divides^#)	=	0	status(divides^#)	=	[1, 2]	list-extension(divides^#)	=	Lex
prec(plus)	=	0	status(plus)	=	[]	list-extension(plus)	=	Lex
prec(if^#)	=	0	status(if^#)	=	[1, 2, 3]	list-extension(if^#)	=	Lex
prec(quot^#)	=	0	status(quot^#)	=	[3, 2, 1]	list-extension(quot^#)	=	Lex
prec(divides)	=	0	status(divides)	=	[1, 2]	list-extension(divides)	=	Lex

and the following Max-polynomial interpretation

[div^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	1
[pr^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[eq(x₁, x₂)]	=	max(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, 0)
[prime^#(x₁)]	=	1
[p(x₁)]	=	x₁ + 0
[0]	=	23676
[quot(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[times(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[pr(x₁, x₂)]	=	x₁ + 1
[divides^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[plus(x₁, x₂)]	=	max(x₂ + 1, 0)
[if^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[quot^#(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[divides(x₁, x₂)]	=	x₁ + x₂ + 1

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)))

(43)

could be deleted.

1.1.5.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.