YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (11ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (98ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (18ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (17ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

f#(f(X)) → c#(f(g(f(X))))T(d(x_1)) → T(x_1)
T(f(X)) → f#(X)T(f(x_1)) → T(x_1)
T(f(g(f(X)))) → f#(g(f(X)))h#(X) → c#(d(X))
T(g(x_1)) → T(x_1)

Rewrite Rules

f(f(X)) → c(f(g(f(X))))c(X) → d(X)
h(X) → c(d(X))

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, h

Strategy

Context-sensitive strategy:
μ(T) = μ(g) = μ(d) = μ(c) = μ(c#) = ∅
μ(f) = μ(f#) = μ(h#) = μ(h) = {1}

The following SCCs where found

T(d(x_1)) → T(x_1)T(f(x_1)) → T(x_1)
T(g(x_1)) → T(x_1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(d(x_1)) → T(x_1)T(f(x_1)) → T(x_1)
T(g(x_1)) → T(x_1)

Rewrite Rules

f(f(X)) → c(f(g(f(X))))c(X) → d(X)
h(X) → c(d(X))

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, h

Strategy

Context-sensitive strategy:
μ(g) = μ(T) = μ(d) = μ(c) = μ(c#) = ∅
μ(f) = μ(f#) = μ(h#) = μ(h) = {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(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(d(x_1)) → T(x_1)T(f(x_1)) → T(x_1)

Rewrite Rules

f(f(X)) → c(f(g(f(X))))c(X) → d(X)
h(X) → c(d(X))

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, h

Strategy

Context-sensitive strategy:
μ(T) = μ(g) = μ(d) = μ(c) = μ(c#) = ∅
μ(f) = μ(f#) = μ(h#) = μ(h) = {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(d(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(f(x_1)) → T(x_1)

Rewrite Rules

f(f(X)) → c(f(g(f(X))))c(X) → d(X)
h(X) → c(d(X))

Original Signature

Termination of terms over the following signature is verified: f, g, d, c, h

Strategy

Context-sensitive strategy:
μ(g) = μ(T) = μ(d) = μ(c) = μ(c#) = ∅
μ(f) = μ(f#) = μ(h#) = μ(h) = {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(x_1)) → T(x_1)