Certification Problem

Input (TPDB TRS_Standard/SK90/2.43)

The rewrite relation of the following TRS is considered.

merge(nil,y) y (1)
merge(x,nil) x (2)
merge(.(x,y),.(u,v)) if(<(x,u),.(x,merge(y,.(u,v))),.(u,merge(.(x,y),v))) (3)
++(nil,y) y (4)
++(.(x,y),z) .(x,++(y,z)) (5)
if(true,x,y) x (6)
if(false,x,y) x (7)

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.
merge#(.(x,y),.(u,v)) if#(<(x,u),.(x,merge(y,.(u,v))),.(u,merge(.(x,y),v))) (8)
merge#(.(x,y),.(u,v)) merge#(y,.(u,v)) (9)
++#(.(x,y),z) ++#(y,z) (10)
merge#(.(x,y),.(u,v)) merge#(.(x,y),v) (11)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.