Certification Problem

Input (TPDB TRS_Standard/Rubio_04/division)

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)
minus(0,Y)	→	0	(4)
minus(s(X),Y)	→	ifMinus(le(s(X),Y),s(X),Y)	(5)
ifMinus(true,s(X),Y)	→	0	(6)
ifMinus(false,s(X),Y)	→	s(minus(X,Y))	(7)
quot(0,s(Y))	→	0	(8)
quot(s(X),s(Y))	→	s(quot(minus(X,Y),s(Y)))	(9)

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)	(10)
minus^#(s(X),Y)	→	le^#(s(X),Y)	(11)
minus^#(s(X),Y)	→	ifMinus^#(le(s(X),Y),s(X),Y)	(12)
ifMinus^#(false,s(X),Y)	→	minus^#(X,Y)	(13)
quot^#(s(X),s(Y))	→	minus^#(X,Y)	(14)
quot^#(s(X),s(Y))	→	quot^#(minus(X,Y),s(Y))	(15)

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

(15)

1.1.1 Reduction Pair Processor with Usable Rules

Using the

prec(quot^#)	=	0		stat(quot^#)	=	lex
prec(ifMinus)	=	0		stat(ifMinus)	=	lex
prec(minus)	=	0		stat(minus)	=	lex
prec(false)	=	0		stat(false)	=	lex
prec(s)	=	1		stat(s)	=	lex
prec(true)	=	0		stat(true)	=	lex
prec(le)	=	0		stat(le)	=	lex
prec(0)	=	0		stat(0)	=	lex

π(quot^#)	=	1
π(ifMinus)	=	2
π(minus)	=	1
π(false)	=	[]
π(s)	=	[1]
π(true)	=	[]
π(le)	=	[]
π(0)	=	[]

together with the usable rules

minus(0,Y)	→	0	(4)
minus(s(X),Y)	→	ifMinus(le(s(X),Y),s(X),Y)	(5)
ifMinus(true,s(X),Y)	→	0	(6)
ifMinus(false,s(X),Y)	→	s(minus(X,Y))	(7)

(w.r.t. the implicit argument filter of the reduction pair), the pair

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

→

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

(15)

could be deleted.

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

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

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

2 ≥ 3

1 ≥ 2

ifMinus^#(false,s(X),Y) → minus^#(X,Y) (13)

3 ≥ 2

2 > 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) (10)

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

2 > 2

1 > 1

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