---

Step * 2 of Lemma last-data-stream


1. L : Top List
2. ¬(L = [] ∈ (Top List))
3. P : Top
⊢ last(data-stream(P;L)) ~ snd(P*(firstn(||L|| - 1;L))(last(L)))
BY
{ (Unfold `last` 0
   THEN RWO "select-data-stream" 0
   THEN Try (Complete (Auto))
   THEN (RWO "length-data-stream" 0 THENA Auto)
   THEN Try (AutoSplit))⋅ }

1
1. L : Top List
2. ¬(L = [] ∈ (Top List))
3. P : Top
⊢ ||L|| - 1 ∈ ℕ

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  \mneg{}(L  =  [])
3.  P  :  Top
\mvdash{}  last(data-stream(P;L))  \msim{}  snd(P*(firstn(||L||  -  1;L))(last(L)))


By

---

Latex:
(Unfold  `last`  0
  THEN  RWO  "select-data-stream"  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "length-data-stream"  0  THENA  Auto)
  THEN  Try  (AutoSplit))\mcdot{}

---

Home Index