The TRS could be proven terminating. The proof took 51 ms.
Problem 1 was processed with processor DependencyGraph (7ms). | – Problem 2 was processed with processor SubtermCriterion (0ms).
| merge#(++(x, y), ++(u, v)) | → | merge#(++(x, y), v) | merge#(++(x, y), ++(u, v)) | → | merge#(y, ++(u, v)) |
| merge(x, nil) | → | x | merge(nil, y) | → | y | |
| merge(++(x, y), ++(u, v)) | → | ++(x, merge(y, ++(u, v))) | merge(++(x, y), ++(u, v)) | → | ++(u, merge(++(x, y), v)) |
Termination of terms over the following signature is verified: v, u, merge, ++, nil
| merge#(++(x, y), ++(u, v)) → merge#(y, ++(u, v)) |
| merge#(++(x, y), ++(u, v)) | → | merge#(y, ++(u, v)) |
| merge(x, nil) | → | x | merge(nil, y) | → | y | |
| merge(++(x, y), ++(u, v)) | → | ++(x, merge(y, ++(u, v))) | merge(++(x, y), ++(u, v)) | → | ++(u, merge(++(x, y), v)) |
Termination of terms over the following signature is verified: v, u, merge, ++, nil
The following projection was used:
Thus, the following dependency pairs are removed:
| merge#(++(x, y), ++(u, v)) | → | merge#(y, ++(u, v)) |