**Term Rewriting System** *R*:

**[***x*, *y*]

gcd(*x*, 0) -> *x*

gcd(0, *y*) -> *y*

gcd(s(*x*), s(*y*)) -> if(< (*x*, *y*), gcd(s(*x*), -(*y*, *x*)), gcd(-(*x*, *y*), s(*y*)))

**Innermost Termination** of *R* to be shown.

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

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

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

*R* contains **no** SCCs.

**Innermost Termination** of *R* successfully shown.

Duration:

0:00 minutes