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