Certification Problem

Input (TPDB TRS_Standard/AG01/#3.5a)

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)
mod(0,y)	→	0	(7)
mod(s(x),0)	→	0	(8)
mod(s(x),s(y))	→	if_mod(le(y,x),s(x),s(y))	(9)
if_mod(true,s(x),s(y))	→	mod(minus(x,y),s(y))	(10)
if_mod(false,s(x),s(y))	→	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)
mod^#(s(x),s(y))	→	le^#(y,x)	(15)
mod^#(s(x),s(y))	→	if_mod^#(le(y,x),s(x),s(y))	(16)
if_mod^#(true,s(x),s(y))	→	minus^#(x,y)	(17)
if_mod^#(true,s(x),s(y))	→	mod^#(minus(x,y),s(y))	(18)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

if_mod^#(true,s(x),s(y))	→	mod^#(minus(x,y),s(y))	(18)
mod^#(s(x),s(y))	→	if_mod^#(le(y,x),s(x),s(y))	(16)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(if_mod^#)	=	{ 2 }
π(mod^#)	=	{ 1 }
π(minus)	=	{ 1 }
π(pred)	=	{ 1 }

to remove the pairs:

if_mod^#(true,s(x),s(y))

→

mod^#(minus(x,y),s(y))

(18)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

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.