WORST_CASE(Omega(n^1),?)
proof of input_ssdYutM4eX.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 1 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 437 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 218 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 178 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 2795 ms]
        (22) BOUNDS(1, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   filter(cons(X, Y), 0, M) -> cons(0, filter(Y, M, M))
   filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
   sieve(cons(0, Y)) -> cons(0, sieve(Y))
   sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
   nats(N) -> cons(N, nats(s(N)))
   zprimes -> sieve(nats(s(s(0))))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2))
   filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
   sieve(cons(0, z0)) -> cons(0, sieve(z0))
   sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
   nats(z0) -> cons(z0, nats(s(z0)))
   zprimes -> sieve(nats(s(s(0))))
Tuples:
   FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2))
   FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
   SIEVE(cons(0, z0)) -> c2(SIEVE(z0))
   SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
   NATS(z0) -> c4(NATS(s(z0)))
   ZPRIMES -> c5(SIEVE(nats(s(s(0)))), NATS(s(s(0))))
S tuples:
   FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2))
   FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
   SIEVE(cons(0, z0)) -> c2(SIEVE(z0))
   SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
   NATS(z0) -> c4(NATS(s(z0)))
   ZPRIMES -> c5(SIEVE(nats(s(s(0)))), NATS(s(s(0))))
K tuples:none
Defined Rule Symbols:   filter_3, sieve_1, nats_1, zprimes

Defined Pair Symbols:   FILTER_3, SIEVE_1, NATS_1, ZPRIMES

Compound Symbols:   c_1, c1_1, c2_1, c3_2, c4_1, c5_2


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   FILTER(cons(z0, z1), 0, z2) -> c(FILTER(z1, z2, z2))
   FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
   SIEVE(cons(0, z0)) -> c2(SIEVE(z0))
   SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
   NATS(z0) -> c4(NATS(s(z0)))
   ZPRIMES -> c5(SIEVE(nats(s(s(0)))), NATS(s(s(0))))

The (relative) TRS S consists of the following rules:

   filter(cons(z0, z1), 0, z2) -> cons(0, filter(z1, z2, z2))
   filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
   sieve(cons(0, z0)) -> cons(0, sieve(z0))
   sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
   nats(z0) -> cons(z0, nats(s(z0)))
   zprimes -> sieve(nats(s(s(0))))

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
   FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
   SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
   SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
   NATS(z0) -> c4(NATS(s(z0)))
   ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))

The (relative) TRS S consists of the following rules:

   filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
   filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
   sieve(cons(0', z0)) -> cons(0', sieve(z0))
   sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
   nats(z0) -> cons(z0, nats(s(z0)))
   zprimes -> sieve(nats(s(s(0'))))

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
NATS(z0) -> c4(NATS(s(z0)))
ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))
filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
sieve(cons(0', z0)) -> cons(0', sieve(z0))
sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
nats(z0) -> cons(z0, nats(s(z0)))
zprimes -> sieve(nats(s(s(0'))))

Types:
FILTER :: cons -> 0':s -> 0':s -> c:c1
cons :: 0':s -> cons -> cons
0' :: 0':s
c :: c:c1 -> c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
SIEVE :: cons -> c2:c3
c2 :: c2:c3 -> c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
filter :: cons -> 0':s -> 0':s -> cons
NATS :: 0':s -> c4
c4 :: c4 -> c4
ZPRIMES :: c5
c5 :: c2:c3 -> c4 -> c5
nats :: 0':s -> cons
sieve :: cons -> cons
zprimes :: cons
hole_c:c11_6 :: c:c1
hole_cons2_6 :: cons
hole_0':s3_6 :: 0':s
hole_c2:c34_6 :: c2:c3
hole_c45_6 :: c4
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_cons8_6 :: Nat -> cons
gen_0':s9_6 :: Nat -> 0':s
gen_c2:c310_6 :: Nat -> c2:c3
gen_c411_6 :: Nat -> c4

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
FILTER, SIEVE, filter, NATS, nats, sieve

They will be analysed ascendingly in the following order:
FILTER < SIEVE
filter < SIEVE
filter < sieve

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
NATS(z0) -> c4(NATS(s(z0)))
ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))
filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
sieve(cons(0', z0)) -> cons(0', sieve(z0))
sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
nats(z0) -> cons(z0, nats(s(z0)))
zprimes -> sieve(nats(s(s(0'))))

Types:
FILTER :: cons -> 0':s -> 0':s -> c:c1
cons :: 0':s -> cons -> cons
0' :: 0':s
c :: c:c1 -> c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
SIEVE :: cons -> c2:c3
c2 :: c2:c3 -> c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
filter :: cons -> 0':s -> 0':s -> cons
NATS :: 0':s -> c4
c4 :: c4 -> c4
ZPRIMES :: c5
c5 :: c2:c3 -> c4 -> c5
nats :: 0':s -> cons
sieve :: cons -> cons
zprimes :: cons
hole_c:c11_6 :: c:c1
hole_cons2_6 :: cons
hole_0':s3_6 :: 0':s
hole_c2:c34_6 :: c2:c3
hole_c45_6 :: c4
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_cons8_6 :: Nat -> cons
gen_0':s9_6 :: Nat -> 0':s
gen_c2:c310_6 :: Nat -> c2:c3
gen_c411_6 :: Nat -> c4


Generator Equations:
gen_c:c17_6(0) <=> hole_c:c11_6
gen_c:c17_6(+(x, 1)) <=> c(gen_c:c17_6(x))
gen_cons8_6(0) <=> hole_cons2_6
gen_cons8_6(+(x, 1)) <=> cons(0', gen_cons8_6(x))
gen_0':s9_6(0) <=> 0'
gen_0':s9_6(+(x, 1)) <=> s(gen_0':s9_6(x))
gen_c2:c310_6(0) <=> hole_c2:c34_6
gen_c2:c310_6(+(x, 1)) <=> c2(gen_c2:c310_6(x))
gen_c411_6(0) <=> hole_c45_6
gen_c411_6(+(x, 1)) <=> c4(gen_c411_6(x))


The following defined symbols remain to be analysed:
FILTER, SIEVE, filter, NATS, nats, sieve

They will be analysed ascendingly in the following order:
FILTER < SIEVE
filter < SIEVE
filter < sieve

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FILTER(gen_cons8_6(+(1, n13_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(n13_6)

Induction Base:
FILTER(gen_cons8_6(+(1, 0)), gen_0':s9_6(0), gen_0':s9_6(0))

Induction Step:
FILTER(gen_cons8_6(+(1, +(n13_6, 1))), gen_0':s9_6(0), gen_0':s9_6(0)) ->_R^Omega(1)
c(FILTER(gen_cons8_6(+(1, n13_6)), gen_0':s9_6(0), gen_0':s9_6(0))) ->_IH
c(*12_6)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
NATS(z0) -> c4(NATS(s(z0)))
ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))
filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
sieve(cons(0', z0)) -> cons(0', sieve(z0))
sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
nats(z0) -> cons(z0, nats(s(z0)))
zprimes -> sieve(nats(s(s(0'))))

Types:
FILTER :: cons -> 0':s -> 0':s -> c:c1
cons :: 0':s -> cons -> cons
0' :: 0':s
c :: c:c1 -> c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
SIEVE :: cons -> c2:c3
c2 :: c2:c3 -> c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
filter :: cons -> 0':s -> 0':s -> cons
NATS :: 0':s -> c4
c4 :: c4 -> c4
ZPRIMES :: c5
c5 :: c2:c3 -> c4 -> c5
nats :: 0':s -> cons
sieve :: cons -> cons
zprimes :: cons
hole_c:c11_6 :: c:c1
hole_cons2_6 :: cons
hole_0':s3_6 :: 0':s
hole_c2:c34_6 :: c2:c3
hole_c45_6 :: c4
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_cons8_6 :: Nat -> cons
gen_0':s9_6 :: Nat -> 0':s
gen_c2:c310_6 :: Nat -> c2:c3
gen_c411_6 :: Nat -> c4


Generator Equations:
gen_c:c17_6(0) <=> hole_c:c11_6
gen_c:c17_6(+(x, 1)) <=> c(gen_c:c17_6(x))
gen_cons8_6(0) <=> hole_cons2_6
gen_cons8_6(+(x, 1)) <=> cons(0', gen_cons8_6(x))
gen_0':s9_6(0) <=> 0'
gen_0':s9_6(+(x, 1)) <=> s(gen_0':s9_6(x))
gen_c2:c310_6(0) <=> hole_c2:c34_6
gen_c2:c310_6(+(x, 1)) <=> c2(gen_c2:c310_6(x))
gen_c411_6(0) <=> hole_c45_6
gen_c411_6(+(x, 1)) <=> c4(gen_c411_6(x))


The following defined symbols remain to be analysed:
FILTER, SIEVE, filter, NATS, nats, sieve

They will be analysed ascendingly in the following order:
FILTER < SIEVE
filter < SIEVE
filter < sieve

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
NATS(z0) -> c4(NATS(s(z0)))
ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))
filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
sieve(cons(0', z0)) -> cons(0', sieve(z0))
sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
nats(z0) -> cons(z0, nats(s(z0)))
zprimes -> sieve(nats(s(s(0'))))

Types:
FILTER :: cons -> 0':s -> 0':s -> c:c1
cons :: 0':s -> cons -> cons
0' :: 0':s
c :: c:c1 -> c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
SIEVE :: cons -> c2:c3
c2 :: c2:c3 -> c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
filter :: cons -> 0':s -> 0':s -> cons
NATS :: 0':s -> c4
c4 :: c4 -> c4
ZPRIMES :: c5
c5 :: c2:c3 -> c4 -> c5
nats :: 0':s -> cons
sieve :: cons -> cons
zprimes :: cons
hole_c:c11_6 :: c:c1
hole_cons2_6 :: cons
hole_0':s3_6 :: 0':s
hole_c2:c34_6 :: c2:c3
hole_c45_6 :: c4
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_cons8_6 :: Nat -> cons
gen_0':s9_6 :: Nat -> 0':s
gen_c2:c310_6 :: Nat -> c2:c3
gen_c411_6 :: Nat -> c4


Lemmas:
FILTER(gen_cons8_6(+(1, n13_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(n13_6)


Generator Equations:
gen_c:c17_6(0) <=> hole_c:c11_6
gen_c:c17_6(+(x, 1)) <=> c(gen_c:c17_6(x))
gen_cons8_6(0) <=> hole_cons2_6
gen_cons8_6(+(x, 1)) <=> cons(0', gen_cons8_6(x))
gen_0':s9_6(0) <=> 0'
gen_0':s9_6(+(x, 1)) <=> s(gen_0':s9_6(x))
gen_c2:c310_6(0) <=> hole_c2:c34_6
gen_c2:c310_6(+(x, 1)) <=> c2(gen_c2:c310_6(x))
gen_c411_6(0) <=> hole_c45_6
gen_c411_6(+(x, 1)) <=> c4(gen_c411_6(x))


The following defined symbols remain to be analysed:
filter, SIEVE, NATS, nats, sieve

They will be analysed ascendingly in the following order:
filter < SIEVE
filter < sieve

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
filter(gen_cons8_6(+(1, n2535_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(0)

Induction Base:
filter(gen_cons8_6(+(1, 0)), gen_0':s9_6(0), gen_0':s9_6(0))

Induction Step:
filter(gen_cons8_6(+(1, +(n2535_6, 1))), gen_0':s9_6(0), gen_0':s9_6(0)) ->_R^Omega(0)
cons(0', filter(gen_cons8_6(+(1, n2535_6)), gen_0':s9_6(0), gen_0':s9_6(0))) ->_IH
cons(0', *12_6)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
NATS(z0) -> c4(NATS(s(z0)))
ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))
filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
sieve(cons(0', z0)) -> cons(0', sieve(z0))
sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
nats(z0) -> cons(z0, nats(s(z0)))
zprimes -> sieve(nats(s(s(0'))))

Types:
FILTER :: cons -> 0':s -> 0':s -> c:c1
cons :: 0':s -> cons -> cons
0' :: 0':s
c :: c:c1 -> c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
SIEVE :: cons -> c2:c3
c2 :: c2:c3 -> c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
filter :: cons -> 0':s -> 0':s -> cons
NATS :: 0':s -> c4
c4 :: c4 -> c4
ZPRIMES :: c5
c5 :: c2:c3 -> c4 -> c5
nats :: 0':s -> cons
sieve :: cons -> cons
zprimes :: cons
hole_c:c11_6 :: c:c1
hole_cons2_6 :: cons
hole_0':s3_6 :: 0':s
hole_c2:c34_6 :: c2:c3
hole_c45_6 :: c4
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_cons8_6 :: Nat -> cons
gen_0':s9_6 :: Nat -> 0':s
gen_c2:c310_6 :: Nat -> c2:c3
gen_c411_6 :: Nat -> c4


Lemmas:
FILTER(gen_cons8_6(+(1, n13_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(n13_6)
filter(gen_cons8_6(+(1, n2535_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(0)


Generator Equations:
gen_c:c17_6(0) <=> hole_c:c11_6
gen_c:c17_6(+(x, 1)) <=> c(gen_c:c17_6(x))
gen_cons8_6(0) <=> hole_cons2_6
gen_cons8_6(+(x, 1)) <=> cons(0', gen_cons8_6(x))
gen_0':s9_6(0) <=> 0'
gen_0':s9_6(+(x, 1)) <=> s(gen_0':s9_6(x))
gen_c2:c310_6(0) <=> hole_c2:c34_6
gen_c2:c310_6(+(x, 1)) <=> c2(gen_c2:c310_6(x))
gen_c411_6(0) <=> hole_c45_6
gen_c411_6(+(x, 1)) <=> c4(gen_c411_6(x))


The following defined symbols remain to be analysed:
SIEVE, NATS, nats, sieve
----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SIEVE(gen_cons8_6(+(1, n7502_6))) -> *12_6, rt in Omega(n7502_6)

Induction Base:
SIEVE(gen_cons8_6(+(1, 0)))

Induction Step:
SIEVE(gen_cons8_6(+(1, +(n7502_6, 1)))) ->_R^Omega(1)
c2(SIEVE(gen_cons8_6(+(1, n7502_6)))) ->_IH
c2(*12_6)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
FILTER(cons(z0, z1), 0', z2) -> c(FILTER(z1, z2, z2))
FILTER(cons(z0, z1), s(z2), z3) -> c1(FILTER(z1, z2, z3))
SIEVE(cons(0', z0)) -> c2(SIEVE(z0))
SIEVE(cons(s(z0), z1)) -> c3(SIEVE(filter(z1, z0, z0)), FILTER(z1, z0, z0))
NATS(z0) -> c4(NATS(s(z0)))
ZPRIMES -> c5(SIEVE(nats(s(s(0')))), NATS(s(s(0'))))
filter(cons(z0, z1), 0', z2) -> cons(0', filter(z1, z2, z2))
filter(cons(z0, z1), s(z2), z3) -> cons(z0, filter(z1, z2, z3))
sieve(cons(0', z0)) -> cons(0', sieve(z0))
sieve(cons(s(z0), z1)) -> cons(s(z0), sieve(filter(z1, z0, z0)))
nats(z0) -> cons(z0, nats(s(z0)))
zprimes -> sieve(nats(s(s(0'))))

Types:
FILTER :: cons -> 0':s -> 0':s -> c:c1
cons :: 0':s -> cons -> cons
0' :: 0':s
c :: c:c1 -> c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
SIEVE :: cons -> c2:c3
c2 :: c2:c3 -> c2:c3
c3 :: c2:c3 -> c:c1 -> c2:c3
filter :: cons -> 0':s -> 0':s -> cons
NATS :: 0':s -> c4
c4 :: c4 -> c4
ZPRIMES :: c5
c5 :: c2:c3 -> c4 -> c5
nats :: 0':s -> cons
sieve :: cons -> cons
zprimes :: cons
hole_c:c11_6 :: c:c1
hole_cons2_6 :: cons
hole_0':s3_6 :: 0':s
hole_c2:c34_6 :: c2:c3
hole_c45_6 :: c4
hole_c56_6 :: c5
gen_c:c17_6 :: Nat -> c:c1
gen_cons8_6 :: Nat -> cons
gen_0':s9_6 :: Nat -> 0':s
gen_c2:c310_6 :: Nat -> c2:c3
gen_c411_6 :: Nat -> c4


Lemmas:
FILTER(gen_cons8_6(+(1, n13_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(n13_6)
filter(gen_cons8_6(+(1, n2535_6)), gen_0':s9_6(0), gen_0':s9_6(0)) -> *12_6, rt in Omega(0)
SIEVE(gen_cons8_6(+(1, n7502_6))) -> *12_6, rt in Omega(n7502_6)


Generator Equations:
gen_c:c17_6(0) <=> hole_c:c11_6
gen_c:c17_6(+(x, 1)) <=> c(gen_c:c17_6(x))
gen_cons8_6(0) <=> hole_cons2_6
gen_cons8_6(+(x, 1)) <=> cons(0', gen_cons8_6(x))
gen_0':s9_6(0) <=> 0'
gen_0':s9_6(+(x, 1)) <=> s(gen_0':s9_6(x))
gen_c2:c310_6(0) <=> hole_c2:c34_6
gen_c2:c310_6(+(x, 1)) <=> c2(gen_c2:c310_6(x))
gen_c411_6(0) <=> hole_c45_6
gen_c411_6(+(x, 1)) <=> c4(gen_c411_6(x))


The following defined symbols remain to be analysed:
NATS, nats, sieve
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sieve(gen_cons8_6(+(1, n78429_6))) -> *12_6, rt in Omega(0)

Induction Base:
sieve(gen_cons8_6(+(1, 0)))

Induction Step:
sieve(gen_cons8_6(+(1, +(n78429_6, 1)))) ->_R^Omega(0)
cons(0', sieve(gen_cons8_6(+(1, n78429_6)))) ->_IH
cons(0', *12_6)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
BOUNDS(1, INF)