NO

The TRS could be proven non-terminating. The proof took 81 ms.

The following reduction sequence is a witness for non-termination:

a# →* a#

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (2ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (0ms), PolynomialLinearRange4 (18ms), DependencyGraph (0ms), ReductionPairSAT (12ms), DependencyGraph (0ms), SizeChangePrinciple (0ms), ForwardNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (0ms), Propagation (1ms)].

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a# → U01#(f(a))a# → a#

Rewrite Rules

a → U01(f(a))U01(b) → b

Original Signature

Termination of terms over the following signature is verified: f, b, a

Strategy

Context-sensitive strategy:
μ(T) = μ(b) = μ(a) = μ(a#) = ∅
μ(f) = μ(U01) = μ(U01#) = {1}

The following SCCs where found

a# → a#