Certification Problem

Input (TPDB TRS_Standard/AProVE_04/IJCAR_26)

The rewrite relation of the following TRS is considered.

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

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

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

eq(0,s(y))	→	false	(18)
eq(0,0)	→	true	(16)
eq(s(x),s(y))	→	eq(x,y)	(19)
eq(s(x),0)	→	false	(17)

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

if^#(false,x,y)	→	pr^#(x,y)	(35)
pr^#(x,s(s(y)))	→	if^#(divides(s(s(y)),x),x,s(y))	(34)

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)

(39)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1091
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	0
[div(x₁, x₂)]	=	x₁ + x₂ + 1
[p^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	x₁ + 0
[prime^#(x₁)]	=	0
[p(x₁)]	=	1912
[times^#(x₁, x₂)]	=	0
[0]	=	1089
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[times(x₁, x₂)]	=	1088
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + 27374
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	x₁ + 1088

together with the usable rules

eq(0,s(y))	→	false	(18)
eq(0,0)	→	true	(16)
eq(s(x),s(y))	→	eq(x,y)	(19)
eq(s(x),0)	→	false	(17)

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

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

→

eq^#(x,y)

(39)

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))	(45)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(40)
quot^#(x,0,s(z))	→	div^#(x,s(z))	(29)
div^#(x,y)	→	quot^#(x,y,y)	(27)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1091
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	0
[div(x₁, x₂)]	=	x₁ + x₂ + 1
[p^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	1912
[times^#(x₁, x₂)]	=	0
[0]	=	1089
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[times(x₁, x₂)]	=	23
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + 26309
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	x₁ + 0
[divides(x₁, x₂)]	=	x₁ + 23

together with the usable rules

eq(0,s(y))	→	false	(18)
eq(0,0)	→	true	(16)
eq(s(x),s(y))	→	eq(x,y)	(19)
eq(s(x),0)	→	false	(17)

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

div^#(div(x,y),z)	→	div^#(x,times(y,z))	(45)
quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(40)

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))	(29)
div^#(x,y)	→	quot^#(x,y,y)	(27)

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

(29)

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)

(36)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

eq(0,s(y))	→	false	(18)
eq(0,0)	→	true	(16)
eq(s(x),s(y))	→	eq(x,y)	(19)
eq(s(x),0)	→	false	(17)

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

times^#(s(x),y)

→

times^#(x,y)

(36)

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

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	1
[s(x₁)]	=	x₁ + 30405
[prime(x₁)]	=	0
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[pr^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	0
[div(x₁, x₂)]	=	x₁ + x₂ + 29534
[p^#(x₁)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[prime^#(x₁)]	=	0
[p(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	0
[0]	=	29536
[if(x₁, x₂, x₃)]	=	0
[quot(x₁, x₂, x₃)]	=	x₂ + x₃ + 30402
[times(x₁, x₂)]	=	x₂ + 29535
[pr(x₁, x₂)]	=	0
[divides^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 18588
[if^#(x₁, x₂, x₃)]	=	1
[quot^#(x₁, x₂, x₃)]	=	0
[divides(x₁, x₂)]	=	x₁ + 29535

together with the usable rules

eq(0,s(y))	→	false	(18)
p(s(x))	→	x	(1)
eq(0,0)	→	true	(16)
eq(s(x),s(y))	→	eq(x,y)	(19)
eq(s(x),0)	→	false	(17)

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

plus^#(s(x),y)

→

plus^#(x,y)

(33)

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

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

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

and the following Max-polynomial interpretation

[div^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[s(x₁)]	=	x₁ + 39
[prime(x₁)]	=	1
[plus^#(x₁, x₂)]	=	max(x₁ + 0, 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, x₂ + 1, 0)
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[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₁ + x₂ + 1
[divides^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[plus(x₁, x₂)]	=	max(x₁ + 1, 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 rule

p(s(x))

→

(1)

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

plus^#(s(x),y)

→

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

(32)

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

(41)

1.1.5.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

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

and the following Max-polynomial interpretation

[div^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	1
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 7720, 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, x₂ + 1, 0)
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[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₁ + x₂ + 1
[divides^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[plus(x₁, x₂)]	=	max(x₁ + 1, 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 rule

p(s(x))

→

(1)

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

plus^#(x,s(y))

→

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

(41)

could be deleted.

1.1.5.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.