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.