Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_Zan97_L)

The rewrite relation of the following TRS is considered.

g	→	h	(1)
c	→	d	(2)
h	→	g	(3)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	g
	→	h
	→	g
	=	t₂

where t₂ = t₀