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 ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

-^#(s(x),s(y))	→	-^#(x,y)	(12)
lt^#(s(x),s(y))	→	lt^#(x,y)	(13)
div^#(s(x),s(y))	→	-^#(x,y)	(14)
div^#(s(x),s(y))	→	div^#(-(x,y),s(y))	(15)
div^#(s(x),s(y))	→	lt^#(x,y)	(16)
div^#(s(x),s(y))	→	if^#(lt(x,y),0,s(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))

(15)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(div^#)	=	{ 1 }
π(-)	=	{ 1 }

to remove the pairs:

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

→

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

(15)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair
lt^#(s(x),s(y)) → lt^#(x,y) (13)

1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

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

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair
-^#(s(x),s(y)) → -^#(x,y) (12)

1.1.3 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

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

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.