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