Runtime Complexity TRS:
The TRS R consists of the following rules:

2nd(cons1(X, cons(Y, Z))) → Y
2nd(cons(X, X1)) → 2nd(cons1(X, activate(X1)))
from(X) → cons(X, n__from(n__s(X)))
from(X) → n__from(X)
s(X) → n__s(X)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(X) → X

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

2nd'(cons1'(X, cons'(Y, Z))) → Y
2nd'(cons'(X, X1)) → 2nd'(cons1'(X, activate'(X1)))
from'(X) → cons'(X, n__from'(n__s'(X)))
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Sliced the following arguments:
cons1'/0

Runtime Complexity TRS:
The TRS R consists of the following rules:

2nd'(cons1'(cons'(Y, Z))) → Y
2nd'(cons'(X, X1)) → 2nd'(cons1'(activate'(X1)))
from'(X) → cons'(X, n__from'(n__s'(X)))
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
2nd'(cons1'(cons'(Y, Z))) → Y
2nd'(cons'(X, X1)) → 2nd'(cons1'(activate'(X1)))
from'(X) → cons'(X, n__from'(n__s'(X)))
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Types:
2nd' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
cons1' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
cons' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
activate' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
from' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
n__from' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
n__s' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
s' :: cons':cons1':n__s':n__from' → cons':cons1':n__s':n__from'
_hole_cons':cons1':n__s':n__from'1 :: cons':cons1':n__s':n__from'
_gen_cons':cons1':n__s':n__from'2 :: Nat → cons':cons1':n__s':n__from'

Heuristically decided to analyse the following defined symbols:
2nd', activate'

They will be analysed ascendingly in the following order:
activate' < 2nd'

Generator Equations:
_gen_cons':cons1':n__s':n__from'2(0) ⇔ _hole_cons':cons1':n__s':n__from'1
_gen_cons':cons1':n__s':n__from'2(+(x, 1)) ⇔ cons'(_hole_cons':cons1':n__s':n__from'1, _gen_cons':cons1':n__s':n__from'2(x))

The following defined symbols remain to be analysed:
activate', 2nd'

They will be analysed ascendingly in the following order:
activate' < 2nd'

Could not prove a rewrite lemma for the defined symbol activate'.

The following defined symbols remain to be analysed:
2nd'

Could not prove a rewrite lemma for the defined symbol 2nd'.

No more defined symbols left to analyse.