The TRS could be proven terminating. The proof took 47 ms.
Problem 1 was processed with processor DependencyGraph (2ms).
| T(zeros) | → | zeros# | tail#(cons(X, XS)) | → | T(XS) |
| zeros | → | cons(0, zeros) | tail(cons(X, XS)) | → | XS |
Termination of terms over the following signature is verified: 0, zeros, tail, cons
Context-sensitive strategy:
μ(T) = μ(0) = μ(zeros) = μ(zeros#) = ∅
μ(tail#) = μ(tail) = μ(cons) = {1}