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