a__filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
a__filter(cons(X, Y), s(N), M) → cons(mark(X), filter(Y, N, M))
a__sieve(cons(0, Y)) → cons(0, sieve(Y))
a__sieve(cons(s(N), Y)) → cons(s(mark(N)), sieve(filter(Y, N, N)))
a__nats(N) → cons(mark(N), nats(s(N)))
a__zprimes → a__sieve(a__nats(s(s(0))))
mark(filter(X1, X2, X3)) → a__filter(mark(X1), mark(X2), mark(X3))
mark(sieve(X)) → a__sieve(mark(X))
mark(nats(X)) → a__nats(mark(X))
mark(zprimes) → a__zprimes
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(s(X)) → s(mark(X))
a__filter(X1, X2, X3) → filter(X1, X2, X3)
a__sieve(X) → sieve(X)
a__nats(X) → nats(X)
a__zprimes → zprimes
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__filter'(cons'(X, Y), 0', M) → cons'(0', filter'(Y, M, M))
a__filter'(cons'(X, Y), s'(N), M) → cons'(mark'(X), filter'(Y, N, M))
a__sieve'(cons'(0', Y)) → cons'(0', sieve'(Y))
a__sieve'(cons'(s'(N), Y)) → cons'(s'(mark'(N)), sieve'(filter'(Y, N, N)))
a__nats'(N) → cons'(mark'(N), nats'(s'(N)))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Sliced the following arguments:
cons'/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Infered types.
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Heuristically decided to analyse the following defined symbols:
mark', a__sieve', a__nats', a__zprimes'
They will be analysed ascendingly in the following order:
mark' = a__sieve'
mark' = a__nats'
mark' = a__zprimes'
a__sieve' = a__nats'
a__sieve' = a__zprimes'
a__nats' = a__zprimes'
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Generator Equations:
_gen_cons':0':s':filter':sieve':nats':zprimes'2(0) ⇔ 0'
_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(x, 1)) ⇔ cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(x))
The following defined symbols remain to be analysed:
a__sieve', mark', a__nats', a__zprimes'
They will be analysed ascendingly in the following order:
mark' = a__sieve'
mark' = a__nats'
mark' = a__zprimes'
a__sieve' = a__nats'
a__sieve' = a__zprimes'
a__nats' = a__zprimes'
Could not prove a rewrite lemma for the defined symbol a__sieve'.
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Generator Equations:
_gen_cons':0':s':filter':sieve':nats':zprimes'2(0) ⇔ 0'
_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(x, 1)) ⇔ cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(x))
The following defined symbols remain to be analysed:
mark', a__nats', a__zprimes'
They will be analysed ascendingly in the following order:
mark' = a__sieve'
mark' = a__nats'
mark' = a__zprimes'
a__sieve' = a__nats'
a__sieve' = a__zprimes'
a__nats' = a__zprimes'
Proved the following rewrite lemma:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24)) → _gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24), rt ∈ Ω(1 + n24)
Induction Base:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(0)) →RΩ(1)
0'
Induction Step:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(_$n25, 1))) →RΩ(1)
cons'(mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_$n25))) →IH
cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_$n25))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Lemmas:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24)) → _gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24), rt ∈ Ω(1 + n24)
Generator Equations:
_gen_cons':0':s':filter':sieve':nats':zprimes'2(0) ⇔ 0'
_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(x, 1)) ⇔ cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(x))
The following defined symbols remain to be analysed:
a__nats', a__sieve', a__zprimes'
They will be analysed ascendingly in the following order:
mark' = a__sieve'
mark' = a__nats'
mark' = a__zprimes'
a__sieve' = a__nats'
a__sieve' = a__zprimes'
a__nats' = a__zprimes'
Could not prove a rewrite lemma for the defined symbol a__nats'.
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Lemmas:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24)) → _gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24), rt ∈ Ω(1 + n24)
Generator Equations:
_gen_cons':0':s':filter':sieve':nats':zprimes'2(0) ⇔ 0'
_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(x, 1)) ⇔ cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(x))
The following defined symbols remain to be analysed:
a__zprimes', a__sieve'
They will be analysed ascendingly in the following order:
mark' = a__sieve'
mark' = a__nats'
mark' = a__zprimes'
a__sieve' = a__nats'
a__sieve' = a__zprimes'
a__nats' = a__zprimes'
Could not prove a rewrite lemma for the defined symbol a__zprimes'.
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Lemmas:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24)) → _gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24), rt ∈ Ω(1 + n24)
Generator Equations:
_gen_cons':0':s':filter':sieve':nats':zprimes'2(0) ⇔ 0'
_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(x, 1)) ⇔ cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(x))
The following defined symbols remain to be analysed:
a__sieve'
They will be analysed ascendingly in the following order:
mark' = a__sieve'
mark' = a__nats'
mark' = a__zprimes'
a__sieve' = a__nats'
a__sieve' = a__zprimes'
a__nats' = a__zprimes'
Could not prove a rewrite lemma for the defined symbol a__sieve'.
Rules:
a__filter'(cons'(X), 0', M) → cons'(0')
a__filter'(cons'(X), s'(N), M) → cons'(mark'(X))
a__sieve'(cons'(0')) → cons'(0')
a__sieve'(cons'(s'(N))) → cons'(s'(mark'(N)))
a__nats'(N) → cons'(mark'(N))
a__zprimes' → a__sieve'(a__nats'(s'(s'(0'))))
mark'(filter'(X1, X2, X3)) → a__filter'(mark'(X1), mark'(X2), mark'(X3))
mark'(sieve'(X)) → a__sieve'(mark'(X))
mark'(nats'(X)) → a__nats'(mark'(X))
mark'(zprimes') → a__zprimes'
mark'(cons'(X1)) → cons'(mark'(X1))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__filter'(X1, X2, X3) → filter'(X1, X2, X3)
a__sieve'(X) → sieve'(X)
a__nats'(X) → nats'(X)
a__zprimes' → zprimes'
Types:
a__filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
cons' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
0' :: cons':0':s':filter':sieve':nats':zprimes'
s' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
mark' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
a__zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
filter' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
sieve' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
nats' :: cons':0':s':filter':sieve':nats':zprimes' → cons':0':s':filter':sieve':nats':zprimes'
zprimes' :: cons':0':s':filter':sieve':nats':zprimes'
_hole_cons':0':s':filter':sieve':nats':zprimes'1 :: cons':0':s':filter':sieve':nats':zprimes'
_gen_cons':0':s':filter':sieve':nats':zprimes'2 :: Nat → cons':0':s':filter':sieve':nats':zprimes'
Lemmas:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24)) → _gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24), rt ∈ Ω(1 + n24)
Generator Equations:
_gen_cons':0':s':filter':sieve':nats':zprimes'2(0) ⇔ 0'
_gen_cons':0':s':filter':sieve':nats':zprimes'2(+(x, 1)) ⇔ cons'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24)) → _gen_cons':0':s':filter':sieve':nats':zprimes'2(_n24), rt ∈ Ω(1 + n24)