YES

The TRS could be proven terminating. The proof took 506 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (26ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (49ms).
 |    | – Problem 4 was processed with processor PolynomialLinearRange4 (46ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4 (111ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(g_1(x_1)) → T(x_1)T(g_1(x)) → g_1#(x)
*top*_0#(g_1(x)) → *top*_0#(f_0(g_1(x)))T(g_1(x)) → g_1#(x)
g_1#(x) → f_1#(g_1(x))*top*_0#(g_1(x)) → g_1#(x)
f_0#(g_1(x)) → f_1#(f_0(g_1(x)))T(f_0(g_1(x))) → f_0#(g_1(x))
T(f_0(x_1)) → T(x_1)*top*_0#(g_1(x)) → f_0#(g_1(x))

Rewrite Rules

f_1(g_1(a_0)) → a_0f_1(f_0(x)) → b_0
f_1(f_1(x)) → b_0g_1(x) → f_1(g_1(x))
*top*_0(g_1(x)) → *top*_0(f_0(g_1(x)))f_0(g_1(x)) → f_1(f_0(g_1(x)))

Original Signature

Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}

The following SCCs where found

*top*_0#(g_1(x)) → *top*_0#(f_0(g_1(x)))
T(g_1(x_1)) → T(x_1)T(f_0(x_1)) → T(x_1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(g_1(x_1)) → T(x_1)T(f_0(x_1)) → T(x_1)

Rewrite Rules

f_1(g_1(a_0)) → a_0f_1(f_0(x)) → b_0
f_1(f_1(x)) → b_0g_1(x) → f_1(g_1(x))
*top*_0(g_1(x)) → *top*_0(f_0(g_1(x)))f_0(g_1(x)) → f_1(f_0(g_1(x)))

Original Signature

Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(g_1#) = μ(f_1) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}

Polynomial Interpretation

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(g_1(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(f_0(x_1)) → T(x_1)

Rewrite Rules

f_1(g_1(a_0)) → a_0f_1(f_0(x)) → b_0
f_1(f_1(x)) → b_0g_1(x) → f_1(g_1(x))
*top*_0(g_1(x)) → *top*_0(f_0(g_1(x)))f_0(g_1(x)) → f_1(f_0(g_1(x)))

Original Signature

Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(b_0) = μ(f_1) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}

Polynomial Interpretation

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(f_0(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

*top*_0#(g_1(x)) → *top*_0#(f_0(g_1(x)))

Rewrite Rules

f_1(g_1(a_0)) → a_0f_1(f_0(x)) → b_0
f_1(f_1(x)) → b_0g_1(x) → f_1(g_1(x))
*top*_0(g_1(x)) → *top*_0(f_0(g_1(x)))f_0(g_1(x)) → f_1(f_0(g_1(x)))

Original Signature

Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(b_0) = μ(g_1#) = μ(f_1) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}

Polynomial Interpretation

Standard Usable rules

f_1(g_1(a_0)) → a_0g_1(x) → f_1(g_1(x))
f_1(f_0(x)) → b_0f_1(f_1(x)) → b_0
f_0(g_1(x)) → f_1(f_0(g_1(x)))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

*top*_0#(g_1(x)) → *top*_0#(f_0(g_1(x)))