---

Step * of Lemma select-data-stream

∀[L:Top List]. ∀[P:Top]. ∀[i:ℕ].  (data-stream(P;L)[i] ~ if i <z ||L|| then snd(P*(firstn(i;L))(L[i])) else ⊥ fi )
BY
{ ((UnivCD THENA Auto) THEN AutoSplit) }

1
1. L : Top List
2. P : Top
3. i : ℕ
4. i < ||L||
⊢ data-stream(P;L)[i] ~ snd(P*(firstn(i;L))(L[i]))

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

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[P:Top].  \mforall{}[i:\mBbbN{}].
    (data-stream(P;L)[i]  \msim{}  if  i  <z  ||L||  then  snd(P*(firstn(i;L))(L[i]))  else  \mbot{}  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  AutoSplit)

---

Home Index