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

f(X) → cons(X, n__f(n__g(X)))
g(0) → s(0)
g(s(X)) → s(s(g(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
f(X) → n__f(X)
g(X) → n__g(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(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:

f'(X) → cons'(X, n__f'(n__g'(X)))
g'(0') → s'(0')
g'(s'(X)) → s'(s'(g'(X)))
sel'(0', cons'(X, Y)) → X
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
f'(X) → n__f'(X)
g'(X) → n__g'(X)
activate'(n__f'(X)) → f'(activate'(X))
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(X) → cons'(X, n__f'(n__g'(X)))
g'(0') → s'(0')
g'(s'(X)) → s'(s'(g'(X)))
sel'(0', cons'(X, Y)) → X
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
f'(X) → n__f'(X)
g'(X) → n__g'(X)
activate'(n__f'(X)) → f'(activate'(X))
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X

Types:
f' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
cons' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
n__f' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
n__g' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
g' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
0' :: n__g':n__f':cons':0':s'
s' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
sel' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
activate' :: n__g':n__f':cons':0':s' → n__g':n__f':cons':0':s'
_hole_n__g':n__f':cons':0':s'1 :: n__g':n__f':cons':0':s'
_gen_n__g':n__f':cons':0':s'2 :: Nat → n__g':n__f':cons':0':s'

Heuristically decided to analyse the following defined symbols:
g', sel', activate'

They will be analysed ascendingly in the following order:
g' < activate'
activate' < sel'

Generator Equations:
_gen_n__g':n__f':cons':0':s'2(0) ⇔ 0'
_gen_n__g':n__f':cons':0':s'2(+(x, 1)) ⇔ cons'(0', _gen_n__g':n__f':cons':0':s'2(x))

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

They will be analysed ascendingly in the following order:
g' < activate'
activate' < sel'

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

Generator Equations:
_gen_n__g':n__f':cons':0':s'2(0) ⇔ 0'
_gen_n__g':n__f':cons':0':s'2(+(x, 1)) ⇔ cons'(0', _gen_n__g':n__f':cons':0':s'2(x))

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

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

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

Generator Equations:
_gen_n__g':n__f':cons':0':s'2(0) ⇔ 0'
_gen_n__g':n__f':cons':0':s'2(+(x, 1)) ⇔ cons'(0', _gen_n__g':n__f':cons':0':s'2(x))

The following defined symbols remain to be analysed:
sel'

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

Generator Equations:
_gen_n__g':n__f':cons':0':s'2(0) ⇔ 0'
_gen_n__g':n__f':cons':0':s'2(+(x, 1)) ⇔ cons'(0', _gen_n__g':n__f':cons':0':s'2(x))

No more defined symbols left to analyse.