---

Step * 1 of Lemma last-data-stream


1. L : Top List
2. P : Top
3. L = [] ∈ (Top List)
⊢ last(data-stream(P;L)) ~ ⊥
BY
{ (DVar `L' THEN Reduce 0) }

1
1. P : Top
2. [] = [] ∈ (Top List)
⊢ last([]) ~ ⊥

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

---

Latex:

---

Latex:

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


By

---

Latex:
(DVar  `L'  THEN  Reduce  0)

---

Home Index