Certification Problem

Input (TPDB TRS_Relative/Mixed_relative_TRS/gcd_many)

The relative rewrite relation R/S is considered where R is the following TRS

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(nil)	→	0	(9)
gcd(cons(x,nil))	→	x	(10)
gcd(cons(0,y))	→	gcd(y)	(11)
gcd(cons(x,cons(y,z)))	→	gcd(cons(-(x,y),cons(y,z)))	(12)

and S is the following TRS.

gcd(cons(x,cons(y,z)))

→

gcd(cons(max(x,y),cons(min(x,y),z)))

(13)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves that R/S is not relative terminating.

t₀	=	gcd(cons(x,cons(y,z)))
	→_R	gcd(cons(-(x,y),cons(y,z)))
	=	t₁

where t₁ = t₀σ and σ = {x/-(x,y), y/y, z/z}