Certification Problem

Input (TPDB TRS_Standard/Rubio_04/quotminus)

The rewrite relation of the following TRS is considered.

plus(0,Y)	→	Y	(1)
plus(s(X),Y)	→	s(plus(X,Y))	(2)
min(X,0)	→	X	(3)
min(s(X),s(Y))	→	min(X,Y)	(4)
min(min(X,Y),Z)	→	min(X,plus(Y,Z))	(5)
quot(0,s(Y))	→	0	(6)
quot(s(X),s(Y))	→	s(quot(min(X,Y),s(Y)))	(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.

plus^#(s(X),Y)	→	plus^#(X,Y)	(8)
min^#(s(X),s(Y))	→	min^#(X,Y)	(9)
min^#(min(X,Y),Z)	→	plus^#(Y,Z)	(10)
min^#(min(X,Y),Z)	→	min^#(X,plus(Y,Z))	(11)
quot^#(s(X),s(Y))	→	min^#(X,Y)	(12)
quot^#(s(X),s(Y))	→	quot^#(min(X,Y),s(Y))	(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^#(min(X,Y),s(Y))

(13)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

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

to remove the pairs:

quot^#(s(X),s(Y))

→

quot^#(min(X,Y),s(Y))

(13)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

min^#(s(X),s(Y)) → min^#(X,Y) (9)

min^#(min(X,Y),Z) → min^#(X,plus(Y,Z)) (11)

1.1.2 Size-Change Termination

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

min^#(s(X),s(Y)) → min^#(X,Y) (9)

2 > 2

1 > 1

min^#(min(X,Y),Z) → min^#(X,plus(Y,Z)) (11)

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

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

2 ≥ 2

1 > 1

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