Certification Problem

Input (TPDB TRS_Standard/Various_04/09)

The rewrite relation of the following TRS is considered.

f(x,y,w,w,a)	→	g1(x,x,y,w)	(1)
f(x,y,w,a,a)	→	g1(y,x,x,w)	(2)
f(x,y,a,a,w)	→	g2(x,y,y,w)	(3)
f(x,y,a,w,w)	→	g2(y,y,x,w)	(4)
g1(x,x,y,a)	→	h(x,y)	(5)
g1(y,x,x,a)	→	h(x,y)	(6)
g2(x,y,y,a)	→	h(x,y)	(7)
g2(y,y,x,a)	→	h(x,y)	(8)
h(x,x)	→	x	(9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

g1^#(y,x,x,a)	→	h^#(x,y)	(10)
f^#(x,y,w,w,a)	→	g1^#(x,x,y,w)	(11)
g2^#(y,y,x,a)	→	h^#(x,y)	(12)
f^#(x,y,a,a,w)	→	g2^#(x,y,y,w)	(13)
g2^#(x,y,y,a)	→	h^#(x,y)	(14)
f^#(x,y,w,a,a)	→	g1^#(y,x,x,w)	(15)
f^#(x,y,a,w,w)	→	g2^#(y,y,x,w)	(16)
g1^#(x,x,y,a)	→	h^#(x,y)	(17)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.