YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

gcd#(s(x), s(y)) → gcd#(s(x), -(y, x))gcd#(s(x), s(y)) → gcd#(-(x, y), s(y))

Rewrite Rules

gcd(x, 0) → xgcd(0, y) → y
gcd(s(x), s(y)) → if(<(x, y), gcd(s(x), -(y, x)), gcd(-(x, y), s(y)))

Original Signature

Termination of terms over the following signature is verified: 0, s, if, gcd, <, -

Strategy

There are no SCCs!