YES

The TRS could be proven terminating. The proof took 16 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

g#(x, a, b) → g#(b, b, a)

Rewrite Rules

g(x, a, b) → g(b, b, a)

Original Signature

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

Strategy

There are no SCCs!