Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
gcd#
(
s
(
x
) ,
s
(
y
) )
→
gcd#
(
s
(
x
) ,
-
(
y
,
x
) )
gcd#
(
s
(
x
) ,
s
(
y
) )
→
gcd#
(
-
(
x
,
y
) ,
s
(
y
) )
1.1: dependency graph processor
The dependency pairs are split into 0 component(s).