YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (31ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (150ms).
 |    | – Problem 3 was processed with processor DependencyGraph (1ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (19ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f_1#(x, x)f_1#(i_0(x), g_1(g_1(x)))g_1#(x)T(x)
T(g_1(x_1))T(x_1)T(g_1(x))g_1#(x)
T(g_1(g_1(x)))g_1#(g_1(x))f_1#(x, i_0(x))f_1#(x, x)
f_1#(x, y)T(x)T(i_0(x_1))T(x_1)

Rewrite Rules

f_1(x, x)f_1(i_0(x), g_1(g_1(x)))f_1(x, y)x
g_1(x)i_0(x)f_1(x, i_0(x))f_1(x, x)
f_1(i_0(x), i_0(g_1(x)))a_0

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}


The following SCCs where found

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

Problem 2: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

g_1#(x)T(x)T(g_1(x_1))T(x_1)
T(g_1(x))g_1#(x)T(g_1(g_1(x)))g_1#(g_1(x))
T(i_0(x_1))T(x_1)

Rewrite Rules

f_1(x, x)f_1(i_0(x), g_1(g_1(x)))f_1(x, y)x
g_1(x)i_0(x)f_1(x, i_0(x))f_1(x, x)
f_1(i_0(x), i_0(g_1(x)))a_0

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}


Polynomial Interpretation

Standard Usable rules

f_1(i_0(x), i_0(g_1(x)))a_0g_1(x)i_0(x)
f_1(x, i_0(x))f_1(x, x)f_1(x, y)x
f_1(x, x)f_1(i_0(x), g_1(g_1(x)))

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)g_1#(x)T(x)

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

T(g_1(g_1(x)))g_1#(g_1(x))T(g_1(x))g_1#(x)
T(i_0(x_1))T(x_1)

Rewrite Rules

f_1(x, x)f_1(i_0(x), g_1(g_1(x)))f_1(x, y)x
g_1(x)i_0(x)f_1(x, i_0(x))f_1(x, x)
f_1(i_0(x), i_0(g_1(x)))a_0

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}


The following SCCs where found

T(i_0(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

T(i_0(x_1))T(x_1)

Rewrite Rules

f_1(x, x)f_1(i_0(x), g_1(g_1(x)))f_1(x, y)x
g_1(x)i_0(x)f_1(x, i_0(x))f_1(x, x)
f_1(i_0(x), i_0(g_1(x)))a_0

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_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(i_0(x_1))T(x_1)