Certification Problem

Input (TPDB TRS_Standard/Rubio_04/gcd)

The rewrite relation of the following TRS is considered.

minus(X,s(Y))	→	pred(minus(X,Y))	(1)
minus(X,0)	→	X	(2)
pred(s(X))	→	X	(3)
le(s(X),s(Y))	→	le(X,Y)	(4)
le(s(X),0)	→	false	(5)
le(0,Y)	→	true	(6)
gcd(0,Y)	→	0	(7)
gcd(s(X),0)	→	s(X)	(8)
gcd(s(X),s(Y))	→	if(le(Y,X),s(X),s(Y))	(9)
if(true,s(X),s(Y))	→	gcd(minus(X,Y),s(Y))	(10)
if(false,s(X),s(Y))	→	gcd(minus(Y,X),s(X))	(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.

minus^#(X,s(Y))	→	minus^#(X,Y)	(12)
minus^#(X,s(Y))	→	pred^#(minus(X,Y))	(13)
le^#(s(X),s(Y))	→	le^#(X,Y)	(14)
gcd^#(s(X),s(Y))	→	le^#(Y,X)	(15)
gcd^#(s(X),s(Y))	→	if^#(le(Y,X),s(X),s(Y))	(16)
if^#(true,s(X),s(Y))	→	minus^#(X,Y)	(17)
if^#(true,s(X),s(Y))	→	gcd^#(minus(X,Y),s(Y))	(18)
if^#(false,s(X),s(Y))	→	minus^#(Y,X)	(19)
if^#(false,s(X),s(Y))	→	gcd^#(minus(Y,X),s(X))	(20)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

if^#(true,s(X),s(Y))	→	gcd^#(minus(X,Y),s(Y))	(18)
gcd^#(s(X),s(Y))	→	if^#(le(Y,X),s(X),s(Y))	(16)
if^#(false,s(X),s(Y))	→	gcd^#(minus(Y,X),s(X))	(20)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(if^#)	=	{ 2, 2, 3 }
π(gcd^#)	=	{ 1, 1, 1, 2 }
π(pred)	=	{ 1 }
π(minus)	=	{ 1, 1, 1 }

to remove the pairs:

if^#(true,s(X),s(Y))	→	gcd^#(minus(X,Y),s(Y))	(18)
gcd^#(s(X),s(Y))	→	if^#(le(Y,X),s(X),s(Y))	(16)
if^#(false,s(X),s(Y))	→	gcd^#(minus(Y,X),s(X))	(20)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair
minus^#(X,s(Y)) → minus^#(X,Y) (12)

1.1.2 Size-Change Termination

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

minus^#(X,s(Y)) → minus^#(X,Y) (12)

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
le^#(s(X),s(Y)) → le^#(X,Y) (14)

1.1.3 Size-Change Termination

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

le^#(s(X),s(Y)) → le^#(X,Y) (14)

2 > 2

1 > 1

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