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

nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(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:

nats' → adx'(zeros')
zeros' → cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(activate'(Y)))
adx'(cons'(X, Y)) → incr'(cons'(activate'(X), n__adx'(activate'(Y))))
hd'(cons'(X, Y)) → activate'(X)
tl'(cons'(X, Y)) → activate'(Y)
0' → n__0'
zeros' → n__zeros'
s'(X) → n__s'(X)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
nats' → adx'(zeros')
zeros' → cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(activate'(Y)))
adx'(cons'(X, Y)) → incr'(cons'(activate'(X), n__adx'(activate'(Y))))
hd'(cons'(X, Y)) → activate'(X)
tl'(cons'(X, Y)) → activate'(Y)
0' → n__0'
zeros' → n__zeros'
s'(X) → n__s'(X)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(X) → X

Types:
nats' :: n__0':n__zeros':cons':n__s':n__incr':n__adx'
adx' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
zeros' :: n__0':n__zeros':cons':n__s':n__incr':n__adx'
cons' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
n__0' :: n__0':n__zeros':cons':n__s':n__incr':n__adx'
n__zeros' :: n__0':n__zeros':cons':n__s':n__incr':n__adx'
incr' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
n__s' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
activate' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
n__incr' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
n__adx' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
hd' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
tl' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
0' :: n__0':n__zeros':cons':n__s':n__incr':n__adx'
s' :: n__0':n__zeros':cons':n__s':n__incr':n__adx' → n__0':n__zeros':cons':n__s':n__incr':n__adx'
_hole_n__0':n__zeros':cons':n__s':n__incr':n__adx'1 :: n__0':n__zeros':cons':n__s':n__incr':n__adx'
_gen_n__0':n__zeros':cons':n__s':n__incr':n__adx'2 :: Nat → n__0':n__zeros':cons':n__s':n__incr':n__adx'

Heuristically decided to analyse the following defined symbols:
adx', incr', activate'

They will be analysed ascendingly in the following order:
adx' = incr'
adx' = activate'
incr' = activate'

Generator Equations:
_gen_n__0':n__zeros':cons':n__s':n__incr':n__adx'2(0) ⇔ n__0'
_gen_n__0':n__zeros':cons':n__s':n__incr':n__adx'2(+(x, 1)) ⇔ cons'(n__0', _gen_n__0':n__zeros':cons':n__s':n__incr':n__adx'2(x))

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

They will be analysed ascendingly in the following order:
adx' = incr'
adx' = activate'
incr' = activate'

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

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

They will be analysed ascendingly in the following order:
adx' = incr'
adx' = activate'
incr' = activate'

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

The following defined symbols remain to be analysed:
adx'

They will be analysed ascendingly in the following order:
adx' = incr'
adx' = activate'
incr' = activate'

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

No more defined symbols left to analyse.