fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, n__fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
fib1(X1, X2) → n__fib1(X1, X2)
activate(n__fib1(X1, X2)) → fib1(X1, X2)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
fib'(N) → sel'(N, fib1'(s'(0'), s'(0')))
fib1'(X, Y) → cons'(X, n__fib1'(Y, add'(X, Y)))
add'(0', X) → X
add'(s'(X), Y) → s'(add'(X, Y))
sel'(0', cons'(X, XS)) → X
sel'(s'(N), cons'(X, XS)) → sel'(N, activate'(XS))
fib1'(X1, X2) → n__fib1'(X1, X2)
activate'(n__fib1'(X1, X2)) → fib1'(X1, X2)
activate'(X) → X
Infered types.
Rules:
fib'(N) → sel'(N, fib1'(s'(0'), s'(0')))
fib1'(X, Y) → cons'(X, n__fib1'(Y, add'(X, Y)))
add'(0', X) → X
add'(s'(X), Y) → s'(add'(X, Y))
sel'(0', cons'(X, XS)) → X
sel'(s'(N), cons'(X, XS)) → sel'(N, activate'(XS))
fib1'(X1, X2) → n__fib1'(X1, X2)
activate'(n__fib1'(X1, X2)) → fib1'(X1, X2)
activate'(X) → X
Types:
fib' :: 0':s' → 0':s'
sel' :: 0':s' → n__fib1':cons' → 0':s'
fib1' :: 0':s' → 0':s' → n__fib1':cons'
s' :: 0':s' → 0':s'
0' :: 0':s'
cons' :: 0':s' → n__fib1':cons' → n__fib1':cons'
n__fib1' :: 0':s' → 0':s' → n__fib1':cons'
add' :: 0':s' → 0':s' → 0':s'
activate' :: n__fib1':cons' → n__fib1':cons'
_hole_0':s'1 :: 0':s'
_hole_n__fib1':cons'2 :: n__fib1':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_n__fib1':cons'4 :: Nat → n__fib1':cons'
Heuristically decided to analyse the following defined symbols:
sel', add'
Rules:
fib'(N) → sel'(N, fib1'(s'(0'), s'(0')))
fib1'(X, Y) → cons'(X, n__fib1'(Y, add'(X, Y)))
add'(0', X) → X
add'(s'(X), Y) → s'(add'(X, Y))
sel'(0', cons'(X, XS)) → X
sel'(s'(N), cons'(X, XS)) → sel'(N, activate'(XS))
fib1'(X1, X2) → n__fib1'(X1, X2)
activate'(n__fib1'(X1, X2)) → fib1'(X1, X2)
activate'(X) → X
Types:
fib' :: 0':s' → 0':s'
sel' :: 0':s' → n__fib1':cons' → 0':s'
fib1' :: 0':s' → 0':s' → n__fib1':cons'
s' :: 0':s' → 0':s'
0' :: 0':s'
cons' :: 0':s' → n__fib1':cons' → n__fib1':cons'
n__fib1' :: 0':s' → 0':s' → n__fib1':cons'
add' :: 0':s' → 0':s' → 0':s'
activate' :: n__fib1':cons' → n__fib1':cons'
_hole_0':s'1 :: 0':s'
_hole_n__fib1':cons'2 :: n__fib1':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_n__fib1':cons'4 :: Nat → n__fib1':cons'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_n__fib1':cons'4(0) ⇔ n__fib1'(0', 0')
_gen_n__fib1':cons'4(+(x, 1)) ⇔ cons'(0', _gen_n__fib1':cons'4(x))
The following defined symbols remain to be analysed:
sel', add'
Proved the following rewrite lemma:
sel'(_gen_0':s'3(_n6), _gen_n__fib1':cons'4(1)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)
Induction Base:
sel'(_gen_0':s'3(0), _gen_n__fib1':cons'4(1)) →RΩ(1)
0'
Induction Step:
sel'(_gen_0':s'3(+(_$n7, 1)), _gen_n__fib1':cons'4(1)) →RΩ(1)
sel'(_gen_0':s'3(_$n7), activate'(_gen_n__fib1':cons'4(0))) →RΩ(1)
sel'(_gen_0':s'3(_$n7), fib1'(0', 0')) →RΩ(1)
sel'(_gen_0':s'3(_$n7), cons'(0', n__fib1'(0', add'(0', 0')))) →RΩ(1)
sel'(_gen_0':s'3(_$n7), cons'(0', n__fib1'(0', 0'))) →IH
_gen_0':s'3(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
fib'(N) → sel'(N, fib1'(s'(0'), s'(0')))
fib1'(X, Y) → cons'(X, n__fib1'(Y, add'(X, Y)))
add'(0', X) → X
add'(s'(X), Y) → s'(add'(X, Y))
sel'(0', cons'(X, XS)) → X
sel'(s'(N), cons'(X, XS)) → sel'(N, activate'(XS))
fib1'(X1, X2) → n__fib1'(X1, X2)
activate'(n__fib1'(X1, X2)) → fib1'(X1, X2)
activate'(X) → X
Types:
fib' :: 0':s' → 0':s'
sel' :: 0':s' → n__fib1':cons' → 0':s'
fib1' :: 0':s' → 0':s' → n__fib1':cons'
s' :: 0':s' → 0':s'
0' :: 0':s'
cons' :: 0':s' → n__fib1':cons' → n__fib1':cons'
n__fib1' :: 0':s' → 0':s' → n__fib1':cons'
add' :: 0':s' → 0':s' → 0':s'
activate' :: n__fib1':cons' → n__fib1':cons'
_hole_0':s'1 :: 0':s'
_hole_n__fib1':cons'2 :: n__fib1':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_n__fib1':cons'4 :: Nat → n__fib1':cons'
Lemmas:
sel'(_gen_0':s'3(_n6), _gen_n__fib1':cons'4(1)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_n__fib1':cons'4(0) ⇔ n__fib1'(0', 0')
_gen_n__fib1':cons'4(+(x, 1)) ⇔ cons'(0', _gen_n__fib1':cons'4(x))
The following defined symbols remain to be analysed:
add'
Proved the following rewrite lemma:
add'(_gen_0':s'3(_n1222), _gen_0':s'3(b)) → _gen_0':s'3(+(_n1222, b)), rt ∈ Ω(1 + n1222)
Induction Base:
add'(_gen_0':s'3(0), _gen_0':s'3(b)) →RΩ(1)
_gen_0':s'3(b)
Induction Step:
add'(_gen_0':s'3(+(_$n1223, 1)), _gen_0':s'3(_b1391)) →RΩ(1)
s'(add'(_gen_0':s'3(_$n1223), _gen_0':s'3(_b1391))) →IH
s'(_gen_0':s'3(+(_$n1223, _b1391)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
fib'(N) → sel'(N, fib1'(s'(0'), s'(0')))
fib1'(X, Y) → cons'(X, n__fib1'(Y, add'(X, Y)))
add'(0', X) → X
add'(s'(X), Y) → s'(add'(X, Y))
sel'(0', cons'(X, XS)) → X
sel'(s'(N), cons'(X, XS)) → sel'(N, activate'(XS))
fib1'(X1, X2) → n__fib1'(X1, X2)
activate'(n__fib1'(X1, X2)) → fib1'(X1, X2)
activate'(X) → X
Types:
fib' :: 0':s' → 0':s'
sel' :: 0':s' → n__fib1':cons' → 0':s'
fib1' :: 0':s' → 0':s' → n__fib1':cons'
s' :: 0':s' → 0':s'
0' :: 0':s'
cons' :: 0':s' → n__fib1':cons' → n__fib1':cons'
n__fib1' :: 0':s' → 0':s' → n__fib1':cons'
add' :: 0':s' → 0':s' → 0':s'
activate' :: n__fib1':cons' → n__fib1':cons'
_hole_0':s'1 :: 0':s'
_hole_n__fib1':cons'2 :: n__fib1':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_n__fib1':cons'4 :: Nat → n__fib1':cons'
Lemmas:
sel'(_gen_0':s'3(_n6), _gen_n__fib1':cons'4(1)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)
add'(_gen_0':s'3(_n1222), _gen_0':s'3(b)) → _gen_0':s'3(+(_n1222, b)), rt ∈ Ω(1 + n1222)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_n__fib1':cons'4(0) ⇔ n__fib1'(0', 0')
_gen_n__fib1':cons'4(+(x, 1)) ⇔ cons'(0', _gen_n__fib1':cons'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
sel'(_gen_0':s'3(_n6), _gen_n__fib1':cons'4(1)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)