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

a__incr(nil) → nil
a__incr(cons(X, L)) → cons(s(mark(X)), incr(L))
a__zeroscons(0, zeros)
a__tail(cons(X, L)) → mark(L)
mark(incr(X)) → a__incr(mark(X))
mark(nats) → a__nats
mark(zeros) → a__zeros
mark(tail(X)) → a__tail(mark(X))
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(0) → 0
a__incr(X) → incr(X)
a__natsnats
a__zeroszeros
a__tail(X) → tail(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__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Heuristically decided to analyse the following defined symbols:

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

Proved the following rewrite lemma:

Induction Base:
nil'

Induction Step:

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

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

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

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

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

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

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

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

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
a__tail'

They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__nats'
a__incr' = a__tail'
mark' = a__nats'
mark' = a__tail'
a__nats' = a__tail'

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

Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__zeros'cons'(0', zeros')
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__nats'nats'
a__zeros'zeros'
a__tail'(X) → tail'(X)

Types: