---

Step * 2 of Lemma select-data-stream


1. L : Top List
2. P : Top
3. i : ℕ
4. ¬i < ||L||
⊢ data-stream(P;L)[i] ~ ⊥
BY
{ (BLemma `select-is-bottom` THEN Try (ProveWfLemma)) }

1
.....wf..... 
1. L : Top List
2. P : Top
3. i : ℕ
4. ¬i < ||L||
⊢ i ∈ ℕ

2
1. L : Top List
2. P : Top
3. i : ℕ
4. ¬i < ||L||
⊢ ||data-stream(P;L)|| ≤ i

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  P  :  Top
3.  i  :  \mBbbN{}
4.  \mneg{}i  <  ||L||
\mvdash{}  data-stream(P;L)[i]  \msim{}  \mbot{}


By

---

Latex:
(BLemma  `select-is-bottom`  THEN  Try  (ProveWfLemma))

---

Home Index