gcd(

gcd(0,

gcd(s(

R

↳Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

R

↳OC

→TRS2

↳Dependency Pair Analysis

GCD(s(x), s(y)) -> GCD(s(x), -(y,x))

GCD(s(x), s(y)) -> GCD(-(x,y), s(y))

Duration:

0:00 minutes