Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/gcd)

The rewrite relation of the following TRS is considered.

min(x,0)	→	0	(1)
min(0,y)	→	0	(2)
min(s(x),s(y))	→	s(min(x,y))	(3)
max(x,0)	→	x	(4)
max(0,y)	→	y	(5)
max(s(x),s(y))	→	s(max(x,y))	(6)
-(x,0)	→	x	(7)
-(s(x),s(y))	→	-(x,y)	(8)
gcd(s(x),0)	→	s(x)	(9)
gcd(0,s(x))	→	s(x)	(10)
gcd(s(x),s(y))	→	gcd(-(max(x,y),min(x,y)),s(min(x,y)))	(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.

min^#(s(x),s(y))	→	min^#(x,y)	(12)
max^#(s(x),s(y))	→	max^#(x,y)	(13)
-^#(s(x),s(y))	→	-^#(x,y)	(14)
gcd^#(s(x),s(y))	→	min^#(x,y)	(15)
gcd^#(s(x),s(y))	→	max^#(x,y)	(16)
gcd^#(s(x),s(y))	→	-^#(max(x,y),min(x,y))	(17)
gcd^#(s(x),s(y))	→	gcd^#(-(max(x,y),min(x,y)),s(min(x,y)))	(18)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

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

→

gcd^#(-(max(x,y),min(x,y)),s(min(x,y)))

(18)

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[-(x₁, x₂)]	=	1 · x₁ + -∞ · x₂ + -∞
[min(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[max(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[0]	=	0
[gcd^#(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + 0
[s(x₁)]	=	3 · x₁ + 4

together with the usable rules

min(x,0)	→	0	(1)
min(0,y)	→	0	(2)
min(s(x),s(y))	→	s(min(x,y))	(3)
max(x,0)	→	x	(4)
max(0,y)	→	y	(5)
max(s(x),s(y))	→	s(max(x,y))	(6)
-(x,0)	→	x	(7)
-(s(x),s(y))	→	-(x,y)	(8)

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

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

→

gcd^#(-(max(x,y),min(x,y)),s(min(x,y)))

(18)

could be deleted.

1.1.1.1 P is empty

There are no pairs anymore.

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

1.1.2 Size-Change Termination

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

-^#(s(x),s(y)) → -^#(x,y) (14)

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
max^#(s(x),s(y)) → max^#(x,y) (13)

1.1.3 Size-Change Termination

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

max^#(s(x),s(y)) → max^#(x,y) (13)

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair
min^#(s(x),s(y)) → min^#(x,y) (12)

1.1.4 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) (12)

2 > 2

1 > 1

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