Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
zWadr#
(
cons
(
X
) ,
cons
(
Y
) )
→
app#
(
Y
,
cons
(
X
) )
1.1: dependency graph processor
The dependency pairs are split into 0 component(s).