2nd(cons(X, n__cons(Y, Z))) → activate(Y)
from(X) → cons(X, n__from(n__s(X)))
cons(X1, X2) → n__cons(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
2nd'(cons'(X, n__cons'(Y, Z))) → activate'(Y)
from'(X) → cons'(X, n__from'(n__s'(X)))
cons'(X1, X2) → n__cons'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X
Infered types.
Rules:
2nd'(cons'(X, n__cons'(Y, Z))) → activate'(Y)
from'(X) → cons'(X, n__from'(n__s'(X)))
cons'(X1, X2) → n__cons'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X
Types:
2nd' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
cons' :: n__cons':n__s':n__from' → n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__cons' :: n__cons':n__s':n__from' → n__cons':n__s':n__from' → n__cons':n__s':n__from'
activate' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
from' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__from' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__s' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
s' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
_hole_n__cons':n__s':n__from'1 :: n__cons':n__s':n__from'
_gen_n__cons':n__s':n__from'2 :: Nat → n__cons':n__s':n__from'
Heuristically decided to analyse the following defined symbols:
activate'
Rules:
2nd'(cons'(X, n__cons'(Y, Z))) → activate'(Y)
from'(X) → cons'(X, n__from'(n__s'(X)))
cons'(X1, X2) → n__cons'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X
Types:
2nd' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
cons' :: n__cons':n__s':n__from' → n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__cons' :: n__cons':n__s':n__from' → n__cons':n__s':n__from' → n__cons':n__s':n__from'
activate' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
from' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__from' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__s' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
s' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
_hole_n__cons':n__s':n__from'1 :: n__cons':n__s':n__from'
_gen_n__cons':n__s':n__from'2 :: Nat → n__cons':n__s':n__from'
Generator Equations:
_gen_n__cons':n__s':n__from'2(0) ⇔ _hole_n__cons':n__s':n__from'1
_gen_n__cons':n__s':n__from'2(+(x, 1)) ⇔ n__cons'(_gen_n__cons':n__s':n__from'2(x), _hole_n__cons':n__s':n__from'1)
The following defined symbols remain to be analysed:
activate'
Proved the following rewrite lemma:
activate'(_gen_n__cons':n__s':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Induction Base:
activate'(_gen_n__cons':n__s':n__from'2(+(1, 0)))
Induction Step:
activate'(_gen_n__cons':n__s':n__from'2(+(1, +(_$n5, 1)))) →RΩ(1)
cons'(activate'(_gen_n__cons':n__s':n__from'2(+(1, _$n5))), _hole_n__cons':n__s':n__from'1) →IH
cons'(_*3, _hole_n__cons':n__s':n__from'1)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
2nd'(cons'(X, n__cons'(Y, Z))) → activate'(Y)
from'(X) → cons'(X, n__from'(n__s'(X)))
cons'(X1, X2) → n__cons'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X
Types:
2nd' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
cons' :: n__cons':n__s':n__from' → n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__cons' :: n__cons':n__s':n__from' → n__cons':n__s':n__from' → n__cons':n__s':n__from'
activate' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
from' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__from' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
n__s' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
s' :: n__cons':n__s':n__from' → n__cons':n__s':n__from'
_hole_n__cons':n__s':n__from'1 :: n__cons':n__s':n__from'
_gen_n__cons':n__s':n__from'2 :: Nat → n__cons':n__s':n__from'
Lemmas:
activate'(_gen_n__cons':n__s':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_n__cons':n__s':n__from'2(0) ⇔ _hole_n__cons':n__s':n__from'1
_gen_n__cons':n__s':n__from'2(+(x, 1)) ⇔ n__cons'(_gen_n__cons':n__s':n__from'2(x), _hole_n__cons':n__s':n__from'1)
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_n__cons':n__s':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)