NO

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

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

f#(a) →* f#(a)

The following DP Processors were used


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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

The following SCCs where found

f#(a) → f#(a)