Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex49_GM04_FR)

The rewrite relation of the following TRS is considered.

minus(n__0,Y)	→	0	(1)
minus(n__s(X),n__s(Y))	→	minus(activate(X),activate(Y))	(2)
geq(X,n__0)	→	true	(3)
geq(n__0,n__s(Y))	→	false	(4)
geq(n__s(X),n__s(Y))	→	geq(activate(X),activate(Y))	(5)
div(0,n__s(Y))	→	0	(6)
div(s(X),n__s(Y))	→	if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(7)
if(true,X,Y)	→	activate(X)	(8)
if(false,X,Y)	→	activate(Y)	(9)
0	→	n__0	(10)
s(X)	→	n__s(X)	(11)
div(X1,X2)	→	n__div(X1,X2)	(12)
minus(X1,X2)	→	n__minus(X1,X2)	(13)
activate(n__0)	→	0	(14)
activate(n__s(X))	→	s(activate(X))	(15)
activate(n__div(X1,X2))	→	div(activate(X1),X2)	(16)
activate(n__minus(X1,X2))	→	minus(X1,X2)	(17)
activate(X)	→	X	(18)

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.

minus^#(n__s(X),n__s(Y))	→	activate^#(X)	(19)
div^#(s(X),n__s(Y))	→	if^#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(20)
geq^#(n__s(X),n__s(Y))	→	activate^#(Y)	(21)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
geq^#(n__s(X),n__s(Y))	→	geq^#(activate(X),activate(Y))	(23)
geq^#(n__s(X),n__s(Y))	→	activate^#(X)	(24)
activate^#(n__minus(X1,X2))	→	minus^#(X1,X2)	(25)
activate^#(n__s(X))	→	activate^#(X)	(26)
div^#(s(X),n__s(Y))	→	geq^#(X,activate(Y))	(27)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
activate^#(n__0)	→	0^#	(28)
minus^#(n__0,Y)	→	0^#	(29)
activate^#(n__s(X))	→	s^#(activate(X))	(30)
activate^#(n__div(X1,X2))	→	activate^#(X1)	(31)
minus^#(n__s(X),n__s(Y))	→	activate^#(Y)	(32)
minus^#(n__s(X),n__s(Y))	→	minus^#(activate(X),activate(Y))	(33)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
activate^#(n__div(X1,X2))	→	div^#(activate(X1),X2)	(34)
if^#(false,X,Y)	→	activate^#(Y)	(35)
if^#(true,X,Y)	→	activate^#(X)	(36)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

if^#(true,X,Y)	→	activate^#(X)	(36)
if^#(false,X,Y)	→	activate^#(Y)	(35)
activate^#(n__minus(X1,X2))	→	minus^#(X1,X2)	(25)
activate^#(n__div(X1,X2))	→	div^#(activate(X1),X2)	(34)
geq^#(n__s(X),n__s(Y))	→	activate^#(X)	(24)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
minus^#(n__s(X),n__s(Y))	→	minus^#(activate(X),activate(Y))	(33)
minus^#(n__s(X),n__s(Y))	→	activate^#(Y)	(32)
activate^#(n__div(X1,X2))	→	activate^#(X1)	(31)
geq^#(n__s(X),n__s(Y))	→	geq^#(activate(X),activate(Y))	(23)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
geq^#(n__s(X),n__s(Y))	→	activate^#(Y)	(21)
div^#(s(X),n__s(Y))	→	if^#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(20)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
div^#(s(X),n__s(Y))	→	geq^#(X,activate(Y))	(27)
minus^#(n__s(X),n__s(Y))	→	activate^#(X)	(19)
activate^#(n__s(X))	→	activate^#(X)	(26)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[div^#(x₁, x₂)]	=	max(x₁ + 4, x₂ + 5, 0)
[s(x₁)]	=	x₁ + 0
[minus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[n__minus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[activate(x₁)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 3, 0)
[activate^#(x₁)]	=	x₁ + 1
[false]	=	0
[div(x₁, x₂)]	=	max(x₁ + 3, x₂ + 4, 0)
[geq(x₁, x₂)]	=	max(0)
[true]	=	0
[n__s(x₁)]	=	x₁ + 0
[n__div(x₁, x₂)]	=	max(x₁ + 3, x₂ + 4, 0)
[0]	=	3
[if(x₁, x₂, x₃)]	=	max(x₁ + 4, x₂ + 0, x₃ + 1, 0)
[s^#(x₁)]	=	0
[n__0]	=	3
[minus^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[if^#(x₁, x₂, x₃)]	=	max(x₁ + 3, x₂ + 1, x₃ + 2, 0)

together with the usable rules

activate(X)	→	X	(18)
geq(n__0,n__s(Y))	→	false	(4)
activate(n__s(X))	→	s(activate(X))	(15)
if(true,X,Y)	→	activate(X)	(8)
minus(n__0,Y)	→	0	(1)
geq(X,n__0)	→	true	(3)
activate(n__div(X1,X2))	→	div(activate(X1),X2)	(16)
activate(n__minus(X1,X2))	→	minus(X1,X2)	(17)
geq(n__s(X),n__s(Y))	→	geq(activate(X),activate(Y))	(5)
0	→	n__0	(10)
div(s(X),n__s(Y))	→	if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(7)
activate(n__0)	→	0	(14)
div(X1,X2)	→	n__div(X1,X2)	(12)
s(X)	→	n__s(X)	(11)
if(false,X,Y)	→	activate(Y)	(9)
minus(X1,X2)	→	n__minus(X1,X2)	(13)
div(0,n__s(Y))	→	0	(6)
minus(n__s(X),n__s(Y))	→	minus(activate(X),activate(Y))	(2)

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

if^#(false,X,Y)	→	activate^#(Y)	(35)
geq^#(n__s(X),n__s(Y))	→	activate^#(X)	(24)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
minus^#(n__s(X),n__s(Y))	→	activate^#(Y)	(32)
activate^#(n__div(X1,X2))	→	activate^#(X1)	(31)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
geq^#(n__s(X),n__s(Y))	→	activate^#(Y)	(21)
div^#(s(X),n__s(Y))	→	activate^#(Y)	(22)
div^#(s(X),n__s(Y))	→	geq^#(X,activate(Y))	(27)

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

geq^#(n__s(X),n__s(Y))

→

geq^#(activate(X),activate(Y))

(23)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[div^#(x₁, x₂)]	=	1
[s(x₁)]	=	x₁ + 45380
[minus(x₁, x₂)]	=	0
[n__minus(x₁, x₂)]	=	0
[activate(x₁)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	x₁ + 1
[activate^#(x₁)]	=	1
[false]	=	2
[div(x₁, x₂)]	=	x₁ + 45545
[geq(x₁, x₂)]	=	1
[true]	=	2
[n__s(x₁)]	=	x₁ + 45380
[n__div(x₁, x₂)]	=	x₁ + 45545
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[s^#(x₁)]	=	0
[n__0]	=	0
[minus^#(x₁, x₂)]	=	1
[if^#(x₁, x₂, x₃)]	=	0

together with the usable rules

activate(X)	→	X	(18)
activate(n__s(X))	→	s(activate(X))	(15)
if(true,X,Y)	→	activate(X)	(8)
minus(n__0,Y)	→	0	(1)
activate(n__div(X1,X2))	→	div(activate(X1),X2)	(16)
activate(n__minus(X1,X2))	→	minus(X1,X2)	(17)
0	→	n__0	(10)
div(s(X),n__s(Y))	→	if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(7)
activate(n__0)	→	0	(14)
div(X1,X2)	→	n__div(X1,X2)	(12)
s(X)	→	n__s(X)	(11)
if(false,X,Y)	→	activate(Y)	(9)
minus(X1,X2)	→	n__minus(X1,X2)	(13)
div(0,n__s(Y))	→	0	(6)
minus(n__s(X),n__s(Y))	→	minus(activate(X),activate(Y))	(2)

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

geq^#(n__s(X),n__s(Y))

→

geq^#(activate(X),activate(Y))

(23)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

activate^#(n__s(X))	→	activate^#(X)	(26)
if^#(true,X,Y)	→	activate^#(X)	(36)
activate^#(n__div(X1,X2))	→	div^#(activate(X1),X2)	(34)
activate^#(n__minus(X1,X2))	→	minus^#(X1,X2)	(25)
div^#(s(X),n__s(Y))	→	if^#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(20)
minus^#(n__s(X),n__s(Y))	→	activate^#(X)	(19)
minus^#(n__s(X),n__s(Y))	→	minus^#(activate(X),activate(Y))	(33)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[div^#(x₁, x₂)]	=	x₁ + 2
[s(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + 0
[n__minus(x₁, x₂)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[geq^#(x₁, x₂)]	=	x₁ + 1
[activate^#(x₁)]	=	x₁ + 1
[false]	=	2
[div(x₁, x₂)]	=	x₁ + 1
[geq(x₁, x₂)]	=	1
[true]	=	2
[n__s(x₁)]	=	x₁ + 1
[n__div(x₁, x₂)]	=	x₁ + 1
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[s^#(x₁)]	=	0
[n__0]	=	0
[minus^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	x₂ + 1

together with the usable rules

activate(X)	→	X	(18)
activate(n__s(X))	→	s(activate(X))	(15)
if(true,X,Y)	→	activate(X)	(8)
minus(n__0,Y)	→	0	(1)
activate(n__div(X1,X2))	→	div(activate(X1),X2)	(16)
activate(n__minus(X1,X2))	→	minus(X1,X2)	(17)
0	→	n__0	(10)
div(s(X),n__s(Y))	→	if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(7)
activate(n__0)	→	0	(14)
div(X1,X2)	→	n__div(X1,X2)	(12)
s(X)	→	n__s(X)	(11)
if(false,X,Y)	→	activate(Y)	(9)
minus(X1,X2)	→	n__minus(X1,X2)	(13)
div(0,n__s(Y))	→	0	(6)
minus(n__s(X),n__s(Y))	→	minus(activate(X),activate(Y))	(2)

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

activate^#(n__s(X))	→	activate^#(X)	(26)
activate^#(n__minus(X1,X2))	→	minus^#(X1,X2)	(25)
minus^#(n__s(X),n__s(Y))	→	minus^#(activate(X),activate(Y))	(33)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

if^#(true,X,Y)	→	activate^#(X)	(36)
activate^#(n__div(X1,X2))	→	div^#(activate(X1),X2)	(34)
div^#(s(X),n__s(Y))	→	if^#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(20)

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[div^#(x₁, x₂)]	=	x₁ + x₂ + 2
[s(x₁)]	=	114
[minus(x₁, x₂)]	=	45671
[n__minus(x₁, x₂)]	=	45671
[activate(x₁)]	=	x₁ + 120
[geq^#(x₁, x₂)]	=	x₁ + 1
[activate^#(x₁)]	=	x₁ + 114
[false]	=	2
[div(x₁, x₂)]	=	x₁ + x₂ + 9
[geq(x₁, x₂)]	=	1
[true]	=	2
[n__s(x₁)]	=	1
[n__div(x₁, x₂)]	=	x₁ + x₂ + 9
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 120
[s^#(x₁)]	=	0
[n__0]	=	0
[minus^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	x₂ + 115

together with the usable rules

activate(X)	→	X	(18)
activate(n__s(X))	→	s(activate(X))	(15)
if(true,X,Y)	→	activate(X)	(8)
minus(n__0,Y)	→	0	(1)
activate(n__div(X1,X2))	→	div(activate(X1),X2)	(16)
activate(n__minus(X1,X2))	→	minus(X1,X2)	(17)
0	→	n__0	(10)
div(s(X),n__s(Y))	→	if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(7)
activate(n__0)	→	0	(14)
div(X1,X2)	→	n__div(X1,X2)	(12)
s(X)	→	n__s(X)	(11)
if(false,X,Y)	→	activate(Y)	(9)
minus(X1,X2)	→	n__minus(X1,X2)	(13)
div(0,n__s(Y))	→	0	(6)
minus(n__s(X),n__s(Y))	→	minus(activate(X),activate(Y))	(2)

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

if^#(true,X,Y)	→	activate^#(X)	(36)
activate^#(n__div(X1,X2))	→	div^#(activate(X1),X2)	(34)
div^#(s(X),n__s(Y))	→	if^#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0)	(20)

could be deleted.

1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.