Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
2nd#
(
cons
(
X
,
n__cons
(
Y
,
Z
) ) )
→
activate#
(
Y
)
from#
(
X
)
→
cons#
(
X
,
n__from
(
s
(
X
) ) )
activate#
(
n__cons
(
X1
,
X2
) )
→
cons#
(
X1
,
X2
)
activate#
(
n__from
(
X
) )
→
from#
(
X
)
1.1: dependency graph processor
The dependency pairs are split into 0 component(s).