---

Step * of Lemma last-data-stream

∀[L:Top List]. ∀[P:Top].  (last(data-stream(P;L)) ~ if null(L) then ⊥ else snd(P*(firstn(||L|| - 1;L))(last(L))) fi )
BY
{ ((UnivCD THENA Auto) THEN AutoSplit) }

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

2
1. L : Top List
2. ¬(L = [] ∈ (Top List))
3. P : Top
⊢ last(data-stream(P;L)) ~ snd(P*(firstn(||L|| - 1;L))(last(L)))

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[P:Top].
    (last(data-stream(P;L))  \msim{}  if  null(L)  then  \mbot{}  else  snd(P*(firstn(||L||  -  1;L))(last(L)))  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  AutoSplit)

---

Home Index