zeros → cons(0, n__zeros)
U11(tt, L) → U12(tt, activate(L))
U12(tt, L) → s(length(activate(L)))
U21(tt, IL, M, N) → U22(tt, activate(IL), activate(M), activate(N))
U22(tt, IL, M, N) → U23(tt, activate(IL), activate(M), activate(N))
U23(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
length(nil) → 0
length(cons(N, L)) → U11(tt, activate(L))
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(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:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
U21'(tt', IL, M, N) → U22'(tt', activate'(IL), activate'(M), activate'(N))
U22'(tt', IL, M, N) → U23'(tt', activate'(IL), activate'(M), activate'(N))
U23'(tt', IL, M, N) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(tt', activate'(L))
take'(0', IL) → nil'
take'(s'(M), cons'(N, IL)) → U21'(tt', activate'(IL), M, N)
zeros' → n__zeros'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__zeros') → zeros'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Infered types.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
U21'(tt', IL, M, N) → U22'(tt', activate'(IL), activate'(M), activate'(N))
U22'(tt', IL, M, N) → U23'(tt', activate'(IL), activate'(M), activate'(N))
U23'(tt', IL, M, N) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(tt', activate'(L))
take'(0', IL) → nil'
take'(s'(M), cons'(N, IL)) → U21'(tt', activate'(IL), M, N)
zeros' → n__zeros'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__zeros') → zeros'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
zeros' :: 0':n__zeros':cons':s':n__take':nil'
cons' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
0' :: 0':n__zeros':cons':s':n__take':nil'
n__zeros' :: 0':n__zeros':cons':s':n__take':nil'
U11' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
tt' :: tt'
U12' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
activate' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
s' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
length' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U21' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U22' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U23' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
n__take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
nil' :: 0':n__zeros':cons':s':n__take':nil'
take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
_hole_0':n__zeros':cons':s':n__take':nil'1 :: 0':n__zeros':cons':s':n__take':nil'
_hole_tt'2 :: tt'
_gen_0':n__zeros':cons':s':n__take':nil'3 :: Nat → 0':n__zeros':cons':s':n__take':nil'
Heuristically decided to analyse the following defined symbols:
activate', length'
They will be analysed ascendingly in the following order:
activate' < length'
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
U21'(tt', IL, M, N) → U22'(tt', activate'(IL), activate'(M), activate'(N))
U22'(tt', IL, M, N) → U23'(tt', activate'(IL), activate'(M), activate'(N))
U23'(tt', IL, M, N) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(tt', activate'(L))
take'(0', IL) → nil'
take'(s'(M), cons'(N, IL)) → U21'(tt', activate'(IL), M, N)
zeros' → n__zeros'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__zeros') → zeros'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
zeros' :: 0':n__zeros':cons':s':n__take':nil'
cons' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
0' :: 0':n__zeros':cons':s':n__take':nil'
n__zeros' :: 0':n__zeros':cons':s':n__take':nil'
U11' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
tt' :: tt'
U12' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
activate' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
s' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
length' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U21' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U22' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U23' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
n__take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
nil' :: 0':n__zeros':cons':s':n__take':nil'
take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
_hole_0':n__zeros':cons':s':n__take':nil'1 :: 0':n__zeros':cons':s':n__take':nil'
_hole_tt'2 :: tt'
_gen_0':n__zeros':cons':s':n__take':nil'3 :: Nat → 0':n__zeros':cons':s':n__take':nil'
Generator Equations:
_gen_0':n__zeros':cons':s':n__take':nil'3(0) ⇔ 0'
_gen_0':n__zeros':cons':s':n__take':nil'3(+(x, 1)) ⇔ cons'(0', _gen_0':n__zeros':cons':s':n__take':nil'3(x))
The following defined symbols remain to be analysed:
activate', length'
They will be analysed ascendingly in the following order:
activate' < length'
Could not prove a rewrite lemma for the defined symbol activate'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
U21'(tt', IL, M, N) → U22'(tt', activate'(IL), activate'(M), activate'(N))
U22'(tt', IL, M, N) → U23'(tt', activate'(IL), activate'(M), activate'(N))
U23'(tt', IL, M, N) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(tt', activate'(L))
take'(0', IL) → nil'
take'(s'(M), cons'(N, IL)) → U21'(tt', activate'(IL), M, N)
zeros' → n__zeros'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__zeros') → zeros'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
zeros' :: 0':n__zeros':cons':s':n__take':nil'
cons' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
0' :: 0':n__zeros':cons':s':n__take':nil'
n__zeros' :: 0':n__zeros':cons':s':n__take':nil'
U11' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
tt' :: tt'
U12' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
activate' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
s' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
length' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U21' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U22' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U23' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
n__take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
nil' :: 0':n__zeros':cons':s':n__take':nil'
take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
_hole_0':n__zeros':cons':s':n__take':nil'1 :: 0':n__zeros':cons':s':n__take':nil'
_hole_tt'2 :: tt'
_gen_0':n__zeros':cons':s':n__take':nil'3 :: Nat → 0':n__zeros':cons':s':n__take':nil'
Generator Equations:
_gen_0':n__zeros':cons':s':n__take':nil'3(0) ⇔ 0'
_gen_0':n__zeros':cons':s':n__take':nil'3(+(x, 1)) ⇔ cons'(0', _gen_0':n__zeros':cons':s':n__take':nil'3(x))
The following defined symbols remain to be analysed:
length'
Proved the following rewrite lemma:
length'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _n27))) → _*4, rt ∈ Ω(n27)
Induction Base:
length'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, 0)))
Induction Step:
length'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, +(_$n28, 1)))) →RΩ(1)
U11'(tt', activate'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _$n28)))) →RΩ(1)
U11'(tt', _gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _$n28))) →RΩ(1)
U12'(tt', activate'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _$n28)))) →RΩ(1)
U12'(tt', _gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _$n28))) →RΩ(1)
s'(length'(activate'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _$n28))))) →RΩ(1)
s'(length'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _$n28)))) →IH
s'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
U21'(tt', IL, M, N) → U22'(tt', activate'(IL), activate'(M), activate'(N))
U22'(tt', IL, M, N) → U23'(tt', activate'(IL), activate'(M), activate'(N))
U23'(tt', IL, M, N) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(tt', activate'(L))
take'(0', IL) → nil'
take'(s'(M), cons'(N, IL)) → U21'(tt', activate'(IL), M, N)
zeros' → n__zeros'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__zeros') → zeros'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
zeros' :: 0':n__zeros':cons':s':n__take':nil'
cons' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
0' :: 0':n__zeros':cons':s':n__take':nil'
n__zeros' :: 0':n__zeros':cons':s':n__take':nil'
U11' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
tt' :: tt'
U12' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
activate' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
s' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
length' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U21' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U22' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
U23' :: tt' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
n__take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
nil' :: 0':n__zeros':cons':s':n__take':nil'
take' :: 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil' → 0':n__zeros':cons':s':n__take':nil'
_hole_0':n__zeros':cons':s':n__take':nil'1 :: 0':n__zeros':cons':s':n__take':nil'
_hole_tt'2 :: tt'
_gen_0':n__zeros':cons':s':n__take':nil'3 :: Nat → 0':n__zeros':cons':s':n__take':nil'
Lemmas:
length'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _n27))) → _*4, rt ∈ Ω(n27)
Generator Equations:
_gen_0':n__zeros':cons':s':n__take':nil'3(0) ⇔ 0'
_gen_0':n__zeros':cons':s':n__take':nil'3(+(x, 1)) ⇔ cons'(0', _gen_0':n__zeros':cons':s':n__take':nil'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
length'(_gen_0':n__zeros':cons':s':n__take':nil'3(+(1, _n27))) → _*4, rt ∈ Ω(n27)