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

dbl(0) → 0
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(n__dbl(activate(X)), n__dbls(activate(Y)))
sel(0, cons(X, Y)) → activate(X)
sel(s(X), cons(Y, Z)) → sel(activate(X), activate(Z))
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z)))
from(X) → cons(activate(X), n__from(n__s(activate(X))))
s(X) → n__s(X)
dbl(X) → n__dbl(X)
dbls(X) → n__dbls(X)
sel(X1, X2) → n__sel(X1, X2)
indx(X1, X2) → n__indx(X1, X2)
from(X) → n__from(X)
activate(n__s(X)) → s(X)
activate(n__dbl(X)) → dbl(X)
activate(n__dbls(X)) → dbls(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__indx(X1, X2)) → indx(X1, X2)
activate(n__from(X)) → from(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:

dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(X)
activate'(n__dbls'(X)) → dbls'(X)
activate'(n__sel'(X1, X2)) → sel'(X1, X2)
activate'(n__indx'(X1, X2)) → indx'(X1, X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(X)
activate'(n__dbls'(X)) → dbls'(X)
activate'(n__sel'(X1, X2)) → sel'(X1, X2)
activate'(n__indx'(X1, X2)) → indx'(X1, X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X

Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'

Heuristically decided to analyse the following defined symbols:
dbl', activate', dbls', sel', from'

They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'

Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))

The following defined symbols remain to be analysed:
activate', dbl', dbls', sel', from'

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

The following defined symbols remain to be analysed:
dbl', dbls', sel', from'

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

The following defined symbols remain to be analysed:
dbls', sel', from'

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

The following defined symbols remain to be analysed:
sel', from'

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

The following defined symbols remain to be analysed:
from'

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

No more defined symbols left to analyse.