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

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__incr'(cons'(X, Y)) → cons'(s'(X), incr'(Y))
a__adx'(cons'(X, Y)) → a__incr'(cons'(X, adx'(Y)))
a__hd'(cons'(X, Y)) → mark'(X)
a__tl'(cons'(X, Y)) → mark'(Y)
mark'(nats') → a__nats'
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(zeros') → a__zeros'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(hd'(X)) → a__hd'(mark'(X))
mark'(tl'(X)) → a__tl'(mark'(X))
mark'(cons'(X1, X2)) → cons'(X1, X2)
mark'(0') → 0'
mark'(s'(X)) → s'(X)
a__nats' → nats'
a__adx'(X) → adx'(X)
a__zeros' → zeros'
a__incr'(X) → incr'(X)
a__hd'(X) → hd'(X)
a__tl'(X) → tl'(X)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
s'/0

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

a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__incr'(cons'(X, Y)) → cons'(s', incr'(Y))
a__adx'(cons'(X, Y)) → a__incr'(cons'(X, adx'(Y)))
a__hd'(cons'(X, Y)) → mark'(X)
a__tl'(cons'(X, Y)) → mark'(Y)
mark'(nats') → a__nats'
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(zeros') → a__zeros'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(hd'(X)) → a__hd'(mark'(X))
mark'(tl'(X)) → a__tl'(mark'(X))
mark'(cons'(X1, X2)) → cons'(X1, X2)
mark'(0') → 0'
mark'(s') → s'
a__nats' → nats'
a__adx'(X) → adx'(X)
a__zeros' → zeros'
a__incr'(X) → incr'(X)
a__hd'(X) → hd'(X)
a__tl'(X) → tl'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__incr'(cons'(X, Y)) → cons'(s', incr'(Y))
a__adx'(cons'(X, Y)) → a__incr'(cons'(X, adx'(Y)))
a__hd'(cons'(X, Y)) → mark'(X)
a__tl'(cons'(X, Y)) → mark'(Y)
mark'(nats') → a__nats'
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(zeros') → a__zeros'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(hd'(X)) → a__hd'(mark'(X))
mark'(tl'(X)) → a__tl'(mark'(X))
mark'(cons'(X1, X2)) → cons'(X1, X2)
mark'(0') → 0'
mark'(s') → s'
a__nats' → nats'
a__adx'(X) → adx'(X)
a__zeros' → zeros'
a__incr'(X) → incr'(X)
a__hd'(X) → hd'(X)
a__tl'(X) → tl'(X)

Types:
a__nats' :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
a__adx' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
a__zeros' :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
cons' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
0' :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
zeros' :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
a__incr' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
s' :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
incr' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
adx' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
a__hd' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
mark' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
a__tl' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
nats' :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
hd' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
tl' :: 0':zeros':cons':s':incr':adx':nats':hd':tl' → 0':zeros':cons':s':incr':adx':nats':hd':tl'
_hole_0':zeros':cons':s':incr':adx':nats':hd':tl'1 :: 0':zeros':cons':s':incr':adx':nats':hd':tl'
_gen_0':zeros':cons':s':incr':adx':nats':hd':tl'2 :: Nat → 0':zeros':cons':s':incr':adx':nats':hd':tl'

Heuristically decided to analyse the following defined symbols:
a__hd', mark', a__tl'

They will be analysed ascendingly in the following order:
a__hd' = mark'
a__hd' = a__tl'
mark' = a__tl'

Generator Equations:
_gen_0':zeros':cons':s':incr':adx':nats':hd':tl'2(0) ⇔ 0'
_gen_0':zeros':cons':s':incr':adx':nats':hd':tl'2(+(x, 1)) ⇔ cons'(0', _gen_0':zeros':cons':s':incr':adx':nats':hd':tl'2(x))

The following defined symbols remain to be analysed:
mark', a__hd', a__tl'

They will be analysed ascendingly in the following order:
a__hd' = mark'
a__hd' = a__tl'
mark' = a__tl'

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

The following defined symbols remain to be analysed:
a__hd', a__tl'

They will be analysed ascendingly in the following order:
a__hd' = mark'
a__hd' = a__tl'
mark' = a__tl'

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

The following defined symbols remain to be analysed:
a__tl'

They will be analysed ascendingly in the following order:
a__hd' = mark'
a__hd' = a__tl'
mark' = a__tl'

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

No more defined symbols left to analyse.