NO

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

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

f#(b) →* f#(b)

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (6ms).
 | – Problem 2 was processed with processor BackwardInstantiation (1ms).
 |    | – Problem 3 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (2ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(X)f#(b)f#(X)b#

Rewrite Rules

f(X)f(b)ba

Original Signature

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

Strategy


The following SCCs where found

f#(X) → f#(b)

Problem 2: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(X)f#(b)

Rewrite Rules

f(X)f(b)ba

Original Signature

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

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(X) → f#(b) on dependency pair chains it holds that: Thus, f#(X) → f#(b) is replaced by instances determined through the above matching. These instances are:
f#(b) → f#(b)