Certification Problem

Input (TPDB TRS_Standard/SK90/2.38)

The rewrite relation of the following TRS is considered.

++(nil,y) y (1)
++(x,nil) x (2)
++(.(x,y),z) .(x,++(y,z)) (3)
++(++(x,y),z) ++(x,++(y,z)) (4)

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.
++#(++(x,y),z) ++#(x,++(y,z)) (5)
++#(++(x,y),z) ++#(y,z) (6)
++#(.(x,y),z) ++#(y,z) (7)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.