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. : ℤ
2. Top List
3. Top
⊢ firstn(0;data-stream(P;L)) data-stream(P;firstn(0;L))

2
1. : ℤ
2. 0 < n
3. ∀[L:Top List]. ∀[P:Top].  (firstn(n 1;data-stream(P;L)) data-stream(P;firstn(n 1;L)))
4. Top List
5. 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