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))))
dbl1(0) → 01
dbl1(s(X)) → s1(s1(dbl1(activate(X))))
sel1(0, cons(X, Y)) → activate(X)
sel1(s(X), cons(Y, Z)) → sel1(activate(X), activate(Z))
quote(0) → 01
quote(s(X)) → s1(quote(activate(X)))
quote(dbl(X)) → dbl1(X)
quote(sel(X, Y)) → sel1(X, Y)
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))))
dbl1'(0') → 01'
dbl1'(s'(X)) → s1'(s1'(dbl1'(activate'(X))))
sel1'(0', cons'(X, Y)) → activate'(X)
sel1'(s'(X), cons'(Y, Z)) → sel1'(activate'(X), activate'(Z))
quote'(0') → 01'
quote'(s'(X)) → s1'(quote'(activate'(X)))
quote'(dbl'(X)) → dbl1'(X)
quote'(sel'(X, Y)) → sel1'(X, Y)
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))))
dbl1'(0') → 01'
dbl1'(s'(X)) → s1'(s1'(dbl1'(activate'(X))))
sel1'(0', cons'(X, Y)) → activate'(X)
sel1'(s'(X), cons'(Y, Z)) → sel1'(activate'(X), activate'(Z))
quote'(0') → 01'
quote'(s'(X)) → s1'(quote'(activate'(X)))
quote'(dbl'(X)) → dbl1'(X)
quote'(sel'(X, Y)) → sel1'(X, Y)
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':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
dbl1' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
01' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
s1' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
sel1' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
quote' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from':01':s1'

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

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

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

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

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

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

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

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

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

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

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

The following defined symbols remain to be analysed:
from', dbl1', sel1', quote'

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

The following defined symbols remain to be analysed:
dbl1', sel1', quote'

They will be analysed ascendingly in the following order:
dbl1' < quote'
sel1' < quote'

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

The following defined symbols remain to be analysed:
sel1', quote'

They will be analysed ascendingly in the following order:
sel1' < quote'

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

The following defined symbols remain to be analysed:
quote'

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

No more defined symbols left to analyse.