The TRS could be proven non-terminating. The proof took 252 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 (0ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (0ms), PolynomialOrdering (72ms), DependencyGraph (1ms), PolynomialOrdering (82ms), DependencyGraph (1ms), PolynomialOrdering (13ms), DependencyGraph (1ms), ReductionPairSAT (12ms), DependencyGraph (0ms), SizeChangePrinciple (2ms), ForwardNarrowing (1ms), 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

Parameters

The following SCCs where found

f#(a) → f#(a)