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

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

zeros'cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(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)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
zeros'cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(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)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(X) → X

Types:

Heuristically decided to analyse the following defined symbols:

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

Rules:
zeros'cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(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)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(X) → X

Types:

Generator Equations:

The following defined symbols remain to be analysed:

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

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

Rules:
zeros'cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(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)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(X) → X

Types:

Generator Equations:

The following defined symbols remain to be analysed:

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

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

Rules:
zeros'cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(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)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(X) → X

Types:

Generator Equations:

The following defined symbols remain to be analysed:

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

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

Rules:
zeros'cons'(n__0', n__zeros')
incr'(cons'(X, Y)) → cons'(n__s'(activate'(X)), n__incr'(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)
activate'(n__0') → 0'
activate'(n__zeros') → zeros'
activate'(n__s'(X)) → s'(X)
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(X) → X

Types: