Certification Problem

Input (TPDB TRS_Standard/Der95/01)

The rewrite relation of the following TRS is considered.

\(x,x)	→	e	(1)
/(x,x)	→	e	(2)
.(e,x)	→	x	(3)
.(x,e)	→	x	(4)
\(e,x)	→	x	(5)
/(x,e)	→	x	(6)
.(x,\(x,y))	→	y	(7)
.(/(y,x),x)	→	y	(8)
\(x,.(x,y))	→	y	(9)
/(.(y,x),x)	→	y	(10)
/(x,\(y,x))	→	y	(11)
\(/(x,y),x)	→	y	(12)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The set of initial dependency pairs is empty, and hence the TRS is terminating.