---

Step * 1 2 of Lemma last-data-stream


1. u : Top
2. v : Top List
3. P : Top
4. [u / v] = [] ∈ (Top List)
⊢ last(data-stream(P;[u / v])) ~ ⊥
BY
{ AutoSimpHyp Auto (-1) }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  P  :  Top
4.  [u  /  v]  =  []
\mvdash{}  last(data-stream(P;[u  /  v]))  \msim{}  \mbot{}


By

---

Latex:
AutoSimpHyp  Auto  (-1)

---

Home Index