Certification Problem

Input (TPDB TRS_Standard/Der95/31)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

:^#(:(x,y),z)	→	:^#(x,:(y,z))	(4)
:^#(:(x,y),z)	→	:^#(y,z)	(5)
:^#(+(x,y),z)	→	:^#(x,z)	(6)
:^#(+(x,y),z)	→	:^#(y,z)	(7)
:^#(z,+(x,f(y)))	→	:^#(g(z,y),+(x,a))	(8)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

:^#(:(x,y),z)	→	:^#(y,z)	(5)
:^#(:(x,y),z)	→	:^#(x,:(y,z))	(4)
:^#(+(x,y),z)	→	:^#(x,z)	(6)
:^#(+(x,y),z)	→	:^#(y,z)	(7)

1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

:^#(:(x,y),z)	→	:^#(y,z)	(5)

1	>	1
2	≥	2
:^#(:(x,y),z)	→	:^#(x,:(y,z))	(4)

1	>	1
:^#(+(x,y),z)	→	:^#(x,z)	(6)

1	>	1
2	≥	2
:^#(+(x,y),z)	→	:^#(y,z)	(7)

1	>	1
2	≥	2

As there is no critical graph in the transitive closure, there are no infinite chains.