YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (9ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (174ms).
 |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (98ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (93ms).
 |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (137ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

g#(0)f#(0)f#(f(x))f#(x)
f#(1)g#(1)g#(0)g#(f(0))
g#(g(x))g#(x)f#(1)f#(g(1))

Rewrite Rules

f(1)f(g(1))f(f(x))f(x)
g(0)g(f(0))g(g(x))g(x)

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0

Strategy


The following SCCs where found

g#(0) → g#(f(0))g#(g(x)) → g#(x)

f#(f(x)) → f#(x)f#(1) → f#(g(1))

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

g#(0)g#(f(0))g#(g(x))g#(x)

Rewrite Rules

f(1)f(g(1))f(f(x))f(x)
g(0)g(f(0))g(g(x))g(x)

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0

Strategy


Polynomial Interpretation

Improved Usable rules

f(1)f(g(1))f(f(x))f(x)

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

g#(g(x))g#(x)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

g#(0)g#(f(0))

Rewrite Rules

f(1)f(g(1))f(f(x))f(x)
g(0)g(f(0))g(g(x))g(x)

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0

Strategy


Polynomial Interpretation

Improved Usable rules

f(1)f(g(1))f(f(x))f(x)

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

g#(0)g#(f(0))

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

f#(f(x))f#(x)f#(1)f#(g(1))

Rewrite Rules

f(1)f(g(1))f(f(x))f(x)
g(0)g(f(0))g(g(x))g(x)

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0

Strategy


Polynomial Interpretation

Improved Usable rules

g(g(x))g(x)g(0)g(f(0))

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

f#(f(x))f#(x)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

f#(1)f#(g(1))

Rewrite Rules

f(1)f(g(1))f(f(x))f(x)
g(0)g(f(0))g(g(x))g(x)

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0

Strategy


Polynomial Interpretation

Improved Usable rules

g(g(x))g(x)g(0)g(f(0))

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

f#(1)f#(g(1))