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 (3ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

h#(x, x, y) → g#(x)g#(a) → h#(a, b, a)
i#(x) → f#(x, x)

Rewrite Rules

f(x, y) → xg(a) → h(a, b, a)
i(x) → f(x, x)h(x, x, y) → g(x)

Original Signature

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

Strategy


There are no SCCs!