Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_AG01/#4.23)

The rewrite relation of the following TRS is considered.

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

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.

quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(6)
plus^#(s(x),y)	→	plus^#(x,y)	(7)
quot^#(x,0,s(z))	→	plus^#(z,s(0))	(8)
quot^#(x,0,s(z))	→	quot^#(x,plus(z,s(0)),s(z))	(9)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

quot^#(s(x),s(y),z)	→	quot^#(x,y,z)	(6)
quot^#(x,0,s(z))	→	quot^#(x,plus(z,s(0)),s(z))	(9)

1.1.1 Subterm Criterion Processor

We use the projection

π(quot^#)

and remove the pairs:

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

→

quot^#(x,y,z)

(6)

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the

prec(quot^#)	=	0	stat(quot^#)	=	lex
prec(plus)	=	1	stat(plus)	=	lex
prec(s)	=	0	stat(s)	=	lex
prec(0)	=	3	stat(0)	=	lex

π(quot^#)	=	[2]
π(plus)	=	[2]
π(s)	=	[]
π(0)	=	[]

together with the usable rules

plus(0,y)	→	y	(3)
plus(s(x),y)	→	s(plus(x,y))	(4)

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

quot^#(x,0,s(z))

→

quot^#(x,plus(z,s(0)),s(z))

(9)

could be deleted.

1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair
plus^#(s(x),y) → plus^#(x,y) (7)

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

2 ≥ 2

1 > 1

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