Certification Problem

Input (TPDB TRS_Standard/SK90/4.06)

The rewrite relation of the following TRS is considered.

((x,y),z)	→	(x,(y,z))	(1)
*(+(x,y),z)	→	+((x,z),(y,z))	(2)
*(x,+(y,f(z)))	→	*(g(x,z),+(y,y))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	*(x48,+(f(z),f(x49)))
	→	*(g(x48,x49),+(f(z),f(z)))
	→	*(g(g(x48,x49),z),+(f(z),f(z)))
	=	t₂

where t₂ = t₀σ and σ = {x49/z, x48/g(g(x48,x49),z), z/z}