YES

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4 (138ms).
 | – Problem 2 was processed with processor DependencyGraph (1ms).

Problem 1: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(f_1(x_1)) → T(x_1)f_1#(x) → g_1#(f_1(x))
g_1#(f_1(x)) → T(x)T(f_1(x)) → f_1#(x)

Rewrite Rules

f_1(x) → g_1(f_1(x))g_1(f_1(x)) → x
g_1(x) → a_0

Original Signature

Termination of terms over the following signature is verified: a_0, g_1, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅

Polynomial Interpretation

Standard Usable rules

g_1(x) → a_0f_1(x) → g_1(f_1(x))
g_1(f_1(x)) → x

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

T(f_1(x_1)) → T(x_1)g_1#(f_1(x)) → T(x)

Problem 2: DependencyGraph

Dependency Pair Problem

Dependency Pairs

f_1#(x) → g_1#(f_1(x))T(f_1(x)) → f_1#(x)

Rewrite Rules

f_1(x) → g_1(f_1(x))g_1(f_1(x)) → x
g_1(x) → a_0

Original Signature

Termination of terms over the following signature is verified: a_0, g_1, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅

There are no SCCs!