Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t014)

The rewrite relation of the following TRS is considered.

-(x,0)	→	x	(1)
-(0,s(y))	→	0	(2)
-(s(x),s(y))	→	-(x,y)	(3)
lt(x,0)	→	false	(4)
lt(0,s(y))	→	true	(5)
lt(s(x),s(y))	→	lt(x,y)	(6)
if(true,x,y)	→	x	(7)
if(false,x,y)	→	y	(8)
div(x,0)	→	0	(9)
div(0,y)	→	0	(10)
div(s(x),s(y))	→	if(lt(x,y),0,s(div(-(x,y),s(y))))	(11)

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.

div^#(s(x),s(y))	→	if^#(lt(x,y),0,s(div(-(x,y),s(y))))	(12)
-^#(s(x),s(y))	→	-^#(x,y)	(13)
div^#(s(x),s(y))	→	-^#(x,y)	(14)
div^#(s(x),s(y))	→	lt^#(x,y)	(15)
lt^#(s(x),s(y))	→	lt^#(x,y)	(16)
div^#(s(x),s(y))	→	div^#(-(x,y),s(y))	(17)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

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

→

div^#(-(x,y),s(y))

(17)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 28959
[lt^#(x₁, x₂)]	=	0
[false]	=	0
[div(x₁, x₂)]	=	0
[true]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	x₁ + 28958
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[lt(x₁, x₂)]	=	0

together with the usable rules

-(x,0)	→	x	(1)
-(s(x),s(y))	→	-(x,y)	(3)
-(0,s(y))	→	0	(2)

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

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

→

div^#(-(x,y),s(y))

(17)

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

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

→

lt^#(x,y)

(16)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 28959
[lt^#(x₁, x₂)]	=	x₁ + x₂ + 0
[false]	=	0
[div(x₁, x₂)]	=	0
[true]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	x₁ + 28958
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[lt(x₁, x₂)]	=	0

together with the usable rules

-(x,0)	→	x	(1)
-(s(x),s(y))	→	-(x,y)	(3)
-(0,s(y))	→	0	(2)

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

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

→

lt^#(x,y)

(16)

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

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

→

-^#(x,y)

(13)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[div^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 28959
[lt^#(x₁, x₂)]	=	0
[false]	=	0
[div(x₁, x₂)]	=	0
[true]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	x₁ + 28958
[-^#(x₁, x₂)]	=	x₁ + x₂ + 0
[if^#(x₁, x₂, x₃)]	=	0
[lt(x₁, x₂)]	=	0

together with the usable rules

-(x,0)	→	x	(1)
-(s(x),s(y))	→	-(x,y)	(3)
-(0,s(y))	→	0	(2)

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

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

→

-^#(x,y)

(13)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.