YES

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

The following DP Processors were used


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

Problem 1: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

dfib#(s(s(x)), y) → dfib#(s(x), dfib(x, y))dfib#(s(s(x)), y) → dfib#(x, y)

Rewrite Rules

dfib(s(s(x)), y) → dfib(s(x), dfib(x, y))

Original Signature

Termination of terms over the following signature is verified: dfib, s

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

dfib#(s(s(x)), y) → dfib#(s(x), dfib(x, y))dfib#(s(s(x)), y) → dfib#(x, y)