The TRS could be proven terminating. The proof took 107 ms.
Problem 1 was processed with processor DependencyGraph (5ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (60ms). | | – Problem 3 was processed with processor DependencyGraph (0ms).
| f_1#(h_0(x)) | → | f_1#(i_1(x)) | T(i_1(x)) | → | i_1#(x) | |
| T(i_1(x_1)) | → | T(x_1) | i_1#(x) | → | T(x) |
| f_1(h_0(x)) | → | f_1(i_1(x)) | f_1(i_1(x)) | → | a_0 | |
| i_1(x) | → | h_0(x) |
Termination of terms over the following signature is verified: h_0, i_1, a_0, f_1
Context-sensitive strategy:
μ(T) = μ(i_1) = μ(f_1#) = μ(a_0) = μ(f_1) = μ(i_1#) = ∅
μ(h_0) = {1}
| T(i_1(x)) → i_1#(x) | T(i_1(x_1)) → T(x_1) |
| i_1#(x) → T(x) |
| T(i_1(x)) | → | i_1#(x) | T(i_1(x_1)) | → | T(x_1) | |
| i_1#(x) | → | T(x) |
| f_1(h_0(x)) | → | f_1(i_1(x)) | f_1(i_1(x)) | → | a_0 | |
| i_1(x) | → | h_0(x) |
Termination of terms over the following signature is verified: h_0, i_1, a_0, f_1
Context-sensitive strategy:
μ(T) = μ(i_1) = μ(a_0) = μ(f_1#) = μ(f_1) = μ(i_1#) = ∅
μ(h_0) = {1}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(i_1(x)) | → | i_1#(x) | T(i_1(x_1)) | → | T(x_1) |
| i_1#(x) | → | T(x) |
| f_1(h_0(x)) | → | f_1(i_1(x)) | f_1(i_1(x)) | → | a_0 | |
| i_1(x) | → | h_0(x) |
Termination of terms over the following signature is verified: h_0, i_1, a_0, f_1
Context-sensitive strategy:
μ(T) = μ(i_1) = μ(f_1#) = μ(a_0) = μ(f_1) = μ(i_1#) = ∅
μ(h_0) = {1}