and(true, X) → activate(X)
and(false, Y) → false
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
add(0, X) → activate(X)
add(s(X), Y) → s(n__add(activate(X), activate(Y)))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(activate(Y), n__first(activate(X), activate(Z)))
from(X) → cons(activate(X), n__from(n__s(activate(X))))
add(X1, X2) → n__add(X1, X2)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
activate(n__add(X1, X2)) → add(activate(X1), X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(X)
activate(n__s(X)) → s(X)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
and'(true', X) → activate'(X)
and'(false', Y) → false'
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
add'(0', X) → activate'(X)
add'(s'(X), Y) → s'(n__add'(activate'(X), activate'(Y)))
first'(0', X) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(activate'(Y), n__first'(activate'(X), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
add'(X1, X2) → n__add'(X1, X2)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__add'(X1, X2)) → add'(activate'(X1), X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X
Infered types.
Rules:
and'(true', X) → activate'(X)
and'(false', Y) → false'
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
add'(0', X) → activate'(X)
add'(s'(X), Y) → s'(n__add'(activate'(X), activate'(Y)))
first'(0', X) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(activate'(Y), n__first'(activate'(X), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
add'(X1, X2) → n__add'(X1, X2)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__add'(X1, X2)) → add'(activate'(X1), X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X
Types:
and' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
true' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
activate' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
false' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
if' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
0' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
nil' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
cons' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_hole_true':false':0':n__add':nil':cons':n__first':n__s':n__from'1 :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2 :: Nat → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
Heuristically decided to analyse the following defined symbols:
activate', from'
They will be analysed ascendingly in the following order:
activate' = from'
Rules:
and'(true', X) → activate'(X)
and'(false', Y) → false'
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
add'(0', X) → activate'(X)
add'(s'(X), Y) → s'(n__add'(activate'(X), activate'(Y)))
first'(0', X) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(activate'(Y), n__first'(activate'(X), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
add'(X1, X2) → n__add'(X1, X2)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__add'(X1, X2)) → add'(activate'(X1), X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X
Types:
and' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
true' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
activate' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
false' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
if' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
0' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
nil' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
cons' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_hole_true':false':0':n__add':nil':cons':n__first':n__s':n__from'1 :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2 :: Nat → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
Generator Equations:
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(0) ⇔ true'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(x, 1)) ⇔ n__add'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(x), true')
The following defined symbols remain to be analysed:
from', activate'
They will be analysed ascendingly in the following order:
activate' = from'
Could not prove a rewrite lemma for the defined symbol from'.
Rules:
and'(true', X) → activate'(X)
and'(false', Y) → false'
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
add'(0', X) → activate'(X)
add'(s'(X), Y) → s'(n__add'(activate'(X), activate'(Y)))
first'(0', X) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(activate'(Y), n__first'(activate'(X), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
add'(X1, X2) → n__add'(X1, X2)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__add'(X1, X2)) → add'(activate'(X1), X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X
Types:
and' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
true' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
activate' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
false' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
if' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
0' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
nil' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
cons' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_hole_true':false':0':n__add':nil':cons':n__first':n__s':n__from'1 :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2 :: Nat → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
Generator Equations:
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(0) ⇔ true'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(x, 1)) ⇔ n__add'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(x), true')
The following defined symbols remain to be analysed:
activate'
They will be analysed ascendingly in the following order:
activate' = from'
Proved the following rewrite lemma:
activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, _n4246))) → _*3, rt ∈ Ω(n4246)
Induction Base:
activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, 0)))
Induction Step:
activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, +(_$n4247, 1)))) →RΩ(1)
add'(activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, _$n4247))), true') →IH
add'(_*3, true')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
and'(true', X) → activate'(X)
and'(false', Y) → false'
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
add'(0', X) → activate'(X)
add'(s'(X), Y) → s'(n__add'(activate'(X), activate'(Y)))
first'(0', X) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(activate'(Y), n__first'(activate'(X), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
add'(X1, X2) → n__add'(X1, X2)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__add'(X1, X2)) → add'(activate'(X1), X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X
Types:
and' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
true' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
activate' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
false' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
if' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
0' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
nil' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
cons' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_hole_true':false':0':n__add':nil':cons':n__first':n__s':n__from'1 :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2 :: Nat → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
Lemmas:
activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, _n4246))) → _*3, rt ∈ Ω(n4246)
Generator Equations:
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(0) ⇔ true'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(x, 1)) ⇔ n__add'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(x), true')
The following defined symbols remain to be analysed:
from'
They will be analysed ascendingly in the following order:
activate' = from'
Could not prove a rewrite lemma for the defined symbol from'.
Rules:
and'(true', X) → activate'(X)
and'(false', Y) → false'
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
add'(0', X) → activate'(X)
add'(s'(X), Y) → s'(n__add'(activate'(X), activate'(Y)))
first'(0', X) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(activate'(Y), n__first'(activate'(X), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
add'(X1, X2) → n__add'(X1, X2)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__add'(X1, X2)) → add'(activate'(X1), X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X
Types:
and' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
true' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
activate' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
false' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
if' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
0' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__add' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
nil' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
cons' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__first' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__from' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
n__s' :: true':false':0':n__add':nil':cons':n__first':n__s':n__from' → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_hole_true':false':0':n__add':nil':cons':n__first':n__s':n__from'1 :: true':false':0':n__add':nil':cons':n__first':n__s':n__from'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2 :: Nat → true':false':0':n__add':nil':cons':n__first':n__s':n__from'
Lemmas:
activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, _n4246))) → _*3, rt ∈ Ω(n4246)
Generator Equations:
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(0) ⇔ true'
_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(x, 1)) ⇔ n__add'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(x), true')
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_true':false':0':n__add':nil':cons':n__first':n__s':n__from'2(+(1, _n4246))) → _*3, rt ∈ Ω(n4246)