---

Step * 1 of Lemma interface-buffer-val


1. Info : Type
2. A : Type
3. es : EO+(Info)
4. n : ℕ
5. X : EClass(A)
6. e : E
7. ↑e ∈b X
⊢ Buffer(n;X)(e) = lastn(n;X(≤(X)(e))) ∈ (A List)
BY
{ (RepUR ``es-interface-buffer eclass-val`` 0⋅ THEN OldAutoSplit) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  es  :  EO+(Info)
4.  n  :  \mBbbN{}
5.  X  :  EClass(A)
6.  e  :  E
7.  \muparrow{}e  \mmember{}\msubb{}  X
\mvdash{}  Buffer(n;X)(e)  =  lastn(n;X(\mleq{}(X)(e)))


By

---

Latex:
(RepUR  ``es-interface-buffer  eclass-val``  0\mcdot{}  THEN  OldAutoSplit)

---

Home Index