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