YES

The TRS could be proven terminating. The proof took 20 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

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

Rewrite Rules

g(f(x), y) → f(h(x, y))h(x, y) → g(x, f(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:

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

Problem 2: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

There are no SCCs!