NO

The TRS could be proven non-terminating. The proof took 200 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 BackwardInstantiation (1ms).
 | – Problem 2 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms), ForwardNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (0ms), Propagation (0ms)].

Problem 1: BackwardInstantiation

Dependency Pair Problem

Dependency Pairs

f#(x) → f#(a)

Rewrite Rules

f(x) → f(a)

Original Signature

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

Strategy

Instantiation

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