YES

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

The following DP Processors were used


Problem 1 was processed with processor SubtermCriterion (0ms).
 | – Problem 2 was processed with processor DependencyGraph (0ms).

Problem 1: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

g#(x, y) → h#(x, y)h#(f(x), y) → g#(x, y)

Rewrite Rules

h(f(x), y) → f(g(x, y))g(x, y) → h(x, y)

Original Signature

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

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

h#(f(x), y) → g#(x, y)

Problem 2: DependencyGraph

Dependency Pair Problem

Dependency Pairs

g#(x, y) → h#(x, y)

Rewrite Rules

h(f(x), y) → f(g(x, y))g(x, y) → h(x, y)

Original Signature

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

Strategy

There are no SCCs!