---

Step * of Lemma firstn-data-stream

∀[n:ℕ]. ∀[L:Top List]. ∀[P:Top].  (firstn(n;data-stream(P;L)) ~ data-stream(P;firstn(n;L)))
BY
{ (InductionOnNat THEN (UnivCD THENA Auto)) }

1
1. n : ℤ
2. L : Top List
3. P : Top
⊢ firstn(0;data-stream(P;L)) ~ data-stream(P;firstn(0;L))

2
1. n : ℤ
2. 0 < n
3. ∀[L:Top List]. ∀[P:Top].  (firstn(n - 1;data-stream(P;L)) ~ data-stream(P;firstn(n - 1;L)))
4. L : Top List
5. P : Top
⊢ firstn(n;data-stream(P;L)) ~ data-stream(P;firstn(n;L))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:Top  List].  \mforall{}[P:Top].    (firstn(n;data-stream(P;L))  \msim{}  data-stream(P;firstn(n;L)))


By

---

Latex:
(InductionOnNat  THEN  (UnivCD  THENA  Auto))

---

Home Index