YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (62ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (178ms).
 |    | – Problem 5 was processed with processor PolynomialLinearRange4 (130ms).
 |    |    | – Problem 7 was processed with processor DependencyGraph (10ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4 (157ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4 (63ms).
 |    | – Problem 6 was processed with processor PolynomialLinearRange4 (17ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f_1#(g_1(a_0))s_0#(g_1(b_0))T(g_1(x))g_1#(x)
*top*_0#(g_1(x))*top*_0#(f_0(g_1(x)))f_1#(g_1(a_0))f_0#(s_0(g_1(b_0)))
g_1#(x)f_1#(g_1(x))f_1#(g_1(a_0))g_1#(b_0)
T(f_0(g_1(x)))f_0#(g_1(x))*top*_0#(g_1(x))f_0#(g_1(x))
T(g_1(x_1))T(x_1)T(g_1(x))g_1#(x)
s_0#(g_1(x))f_0#(g_1(x))*top*_0#(g_1(x))g_1#(x)
s_0#(g_1(x))s_0#(f_0(g_1(x)))s_0#(g_1(x))g_1#(x)
f_0#(g_1(x))f_1#(f_0(g_1(x)))T(f_0(x_1))T(x_1)

Rewrite Rules

f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_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)

f_1#(g_1(a_0)) → s_0#(g_1(b_0))g_1#(x) → f_1#(g_1(x))
f_1#(g_1(a_0)) → g_1#(b_0)s_0#(g_1(x)) → s_0#(f_0(g_1(x)))
s_0#(g_1(x)) → g_1#(x)

Problem 2: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

f_1#(g_1(a_0))s_0#(g_1(b_0))g_1#(x)f_1#(g_1(x))
f_1#(g_1(a_0))g_1#(b_0)s_0#(g_1(x))s_0#(f_0(g_1(x)))
s_0#(g_1(x))g_1#(x)

Rewrite Rules

f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

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


Polynomial Interpretation

Standard Usable rules

g_1(x)f_1(g_1(x))f_1(f_0(x))b_0
f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_1(f_1(x))b_0
s_0(g_1(x))s_0(f_0(g_1(x)))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:

s_0#(g_1(x))s_0#(f_0(g_1(x)))

Problem 5: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

f_1#(g_1(a_0))s_0#(g_1(b_0))g_1#(x)f_1#(g_1(x))
f_1#(g_1(a_0))g_1#(b_0)s_0#(g_1(x))g_1#(x)

Rewrite Rules

f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

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


Polynomial Interpretation

Standard Usable rules

g_1(x)f_1(g_1(x))f_1(f_0(x))b_0
f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_1(f_1(x))b_0
s_0(g_1(x))s_0(f_0(g_1(x)))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:

f_1#(g_1(a_0))s_0#(g_1(b_0))g_1#(x)f_1#(g_1(x))
f_1#(g_1(a_0))g_1#(b_0)

Problem 7: DependencyGraph



Dependency Pair Problem

Dependency Pairs

s_0#(g_1(x))g_1#(x)

Rewrite Rules

f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

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


There are no SCCs!

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))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

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


Polynomial Interpretation

Standard Usable rules

g_1(x)f_1(g_1(x))f_1(f_0(x))b_0
f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_1(f_1(x))b_0
s_0(g_1(x))s_0(f_0(g_1(x)))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)))

Problem 4: 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))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_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 6: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

T(g_1(x_1))T(x_1)

Rewrite Rules

f_1(g_1(a_0))f_0(s_0(g_1(b_0)))f_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)))
s_0(g_1(x))s_0(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, s_0

Strategy

Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_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(g_1(x_1))T(x_1)