Certification Problem

Input (TPDB TRS_Standard/AG01/#3.4)

The rewrite relation of the following TRS is considered.

minus(x,0)	→	x	(1)
minus(s(x),s(y))	→	minus(x,y)	(2)
quot(0,s(y))	→	0	(3)
quot(s(x),s(y))	→	s(quot(minus(x,y),s(y)))	(4)
plus(0,y)	→	y	(5)
plus(s(x),y)	→	s(plus(x,y))	(6)
minus(minus(x,y),z)	→	minus(x,plus(y,z))	(7)

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^#(s(x),s(y))	→	minus^#(x,y)	(8)
quot^#(s(x),s(y))	→	minus^#(x,y)	(9)
quot^#(s(x),s(y))	→	quot^#(minus(x,y),s(y))	(10)
plus^#(s(x),y)	→	plus^#(x,y)	(11)
minus^#(minus(x,y),z)	→	plus^#(y,z)	(12)
minus^#(minus(x,y),z)	→	minus^#(x,plus(y,z))	(13)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

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

→

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

(10)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(quot^#)	=	{ 1 }
π(minus)	=	{ 1 }

to remove the pairs:

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

→

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

(10)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

minus^#(s(x),s(y)) → minus^#(x,y) (8)

minus^#(minus(x,y),z) → minus^#(x,plus(y,z)) (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^#(s(x),s(y)) → minus^#(x,y) (8)

2 > 2

1 > 1

minus^#(minus(x,y),z) → minus^#(x,plus(y,z)) (13)

1 > 1

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

1.1.3 Size-Change Termination

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

plus^#(s(x),y) → plus^#(x,y) (11)

2 ≥ 2

1 > 1

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