Certification Problem

Input (TPDB TRS_Standard/AG01/#3.6)

The rewrite relation of the following TRS is considered.

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

le^#(s(x),s(y))	→	le^#(x,y)	(12)
minus^#(x,s(y))	→	minus^#(x,y)	(13)
minus^#(x,s(y))	→	pred^#(minus(x,y))	(14)
gcd^#(s(x),s(y))	→	le^#(y,x)	(15)
gcd^#(s(x),s(y))	→	if_gcd^#(le(y,x),s(x),s(y))	(16)
if_gcd^#(true,s(x),s(y))	→	minus^#(x,y)	(17)
if_gcd^#(true,s(x),s(y))	→	gcd^#(minus(x,y),s(y))	(18)
if_gcd^#(false,s(x),s(y))	→	minus^#(y,x)	(19)
if_gcd^#(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_gcd^#(false,s(x),s(y))	→	gcd^#(minus(y,x),s(x))	(20)
gcd^#(s(x),s(y))	→	if_gcd^#(le(y,x),s(x),s(y))	(16)
if_gcd^#(true,s(x),s(y))	→	gcd^#(minus(x,y),s(y))	(18)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

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

to remove the pairs:

if_gcd^#(false,s(x),s(y))	→	gcd^#(minus(y,x),s(x))	(20)
gcd^#(s(x),s(y))	→	if_gcd^#(le(y,x),s(x),s(y))	(16)
if_gcd^#(true,s(x),s(y))	→	gcd^#(minus(x,y),s(y))	(18)

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

minus^#(x,s(y)) → minus^#(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
le^#(s(x),s(y)) → le^#(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.

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

2 > 2

1 > 1

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