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

a__fib(N) → a__sel(mark(N), a__fib1(s(0), s(0)))
a__fib1(X, Y) → cons(mark(X), fib1(Y, add(X, Y)))
a__sel(0, cons(X, XS)) → mark(X)
a__sel(s(N), cons(X, XS)) → a__sel(mark(N), mark(XS))
mark(fib(X)) → a__fib(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(fib1(X1, X2)) → a__fib1(mark(X1), mark(X2))
mark(s(X)) → s(mark(X))
mark(0) → 0
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__fib(X) → fib(X)
a__sel(X1, X2) → sel(X1, X2)
a__fib1(X1, X2) → fib1(X1, X2)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Heuristically decided to analyse the following defined symbols:

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

Proved the following rewrite lemma:

Induction Base:
0'

Induction Step:

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

Proved the following rewrite lemma:

Induction Base:

Induction Step:

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
a__sel', a__fib', mark', a__fib1'

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
mark', a__fib', a__fib1'

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

Proved the following rewrite lemma:

Induction Base:
0'

Induction Step:

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
a__fib', a__fib1'

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
a__fib1'

They will be analysed ascendingly in the following order:
a__fib' = a__sel'
a__fib' = mark'
a__fib' = a__fib1'
a__sel' = mark'
a__sel' = a__fib1'
mark' = a__fib1'

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

Rules:
a__fib'(N) → a__sel'(mark'(N), a__fib1'(s'(0'), s'(0')))
a__fib1'(X, Y) → cons'(mark'(X), fib1'(Y, add'(X, Y)))
a__sel'(0', cons'(X, XS)) → mark'(X)
a__sel'(s'(N), cons'(X, XS)) → a__sel'(mark'(N), mark'(XS))
mark'(fib'(X)) → a__fib'(mark'(X))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(fib1'(X1, X2)) → a__fib1'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
a__fib'(X) → fib'(X)
a__sel'(X1, X2) → sel'(X1, X2)
a__fib1'(X1, X2) → fib1'(X1, X2)

Types:

Lemmas: