dbl(0) → 0
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
dbls(nil) → nil
dbls(cons(X, Y)) → cons(n__dbl(activate(X)), n__dbls(activate(Y)))
sel(0, cons(X, Y)) → activate(X)
sel(s(X), cons(Y, Z)) → sel(activate(X), activate(Z))
indx(nil, X) → nil
indx(cons(X, Y), Z) → cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z)))
from(X) → cons(activate(X), n__from(n__s(activate(X))))
s(X) → n__s(X)
dbl(X) → n__dbl(X)
dbls(X) → n__dbls(X)
sel(X1, X2) → n__sel(X1, X2)
indx(X1, X2) → n__indx(X1, X2)
from(X) → n__from(X)
activate(n__s(X)) → s(X)
activate(n__dbl(X)) → dbl(activate(X))
activate(n__dbls(X)) → dbls(activate(X))
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(n__indx(X1, X2)) → indx(activate(X1), X2)
activate(n__from(X)) → from(X)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Infered types.
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Heuristically decided to analyse the following defined symbols:
dbl', activate', dbls', sel', from'
They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))
The following defined symbols remain to be analysed:
activate', dbl', dbls', sel', from'
They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'
Proved the following rewrite lemma:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Induction Base:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, 0)))
Induction Step:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, +(_$n5, 1)))) →RΩ(1)
dbl'(activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _$n5)))) →IH
dbl'(_*3)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Lemmas:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))
The following defined symbols remain to be analysed:
dbl', dbls', sel', from'
They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'
Could not prove a rewrite lemma for the defined symbol dbl'.
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Lemmas:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))
The following defined symbols remain to be analysed:
dbls', sel', from'
They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'
Could not prove a rewrite lemma for the defined symbol dbls'.
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Lemmas:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))
The following defined symbols remain to be analysed:
sel', from'
They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'
Could not prove a rewrite lemma for the defined symbol sel'.
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Lemmas:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))
The following defined symbols remain to be analysed:
from'
They will be analysed ascendingly in the following order:
dbl' = activate'
dbl' = dbls'
dbl' = sel'
dbl' = from'
activate' = dbls'
activate' = sel'
activate' = from'
dbls' = sel'
dbls' = from'
sel' = from'
Could not prove a rewrite lemma for the defined symbol from'.
Rules:
dbl'(0') → 0'
dbl'(s'(X)) → s'(n__s'(n__dbl'(activate'(X))))
dbls'(nil') → nil'
dbls'(cons'(X, Y)) → cons'(n__dbl'(activate'(X)), n__dbls'(activate'(Y)))
sel'(0', cons'(X, Y)) → activate'(X)
sel'(s'(X), cons'(Y, Z)) → sel'(activate'(X), activate'(Z))
indx'(nil', X) → nil'
indx'(cons'(X, Y), Z) → cons'(n__sel'(activate'(X), activate'(Z)), n__indx'(activate'(Y), activate'(Z)))
from'(X) → cons'(activate'(X), n__from'(n__s'(activate'(X))))
s'(X) → n__s'(X)
dbl'(X) → n__dbl'(X)
dbls'(X) → n__dbls'(X)
sel'(X1, X2) → n__sel'(X1, X2)
indx'(X1, X2) → n__indx'(X1, X2)
from'(X) → n__from'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__dbl'(X)) → dbl'(activate'(X))
activate'(n__dbls'(X)) → dbls'(activate'(X))
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(n__indx'(X1, X2)) → indx'(activate'(X1), X2)
activate'(n__from'(X)) → from'(X)
activate'(X) → X
Types:
dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
0' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__s' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbl' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
activate' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
nil' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
cons' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__dbls' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__sel' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__indx' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
n__from' :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from' → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_hole_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'1 :: 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2 :: Nat → 0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'
Lemmas:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(0) ⇔ 0'
_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(x, 1)) ⇔ n__dbl'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_0':n__dbl':n__s':nil':cons':n__dbls':n__sel':n__indx':n__from'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)