YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(a, b) → f#(a, c)f#(c, d) → f#(b, d)

Rewrite Rules

f(a, b) → f(a, c)f(c, d) → f(b, d)

Original Signature

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

Strategy


There are no SCCs!