---

Step * of Lemma interface-buffer-val

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[n:ℕ]. ∀[X:EClass(A)]. ∀[e:E].
  Buffer(n;X)(e) = lastn(n;X(≤(X)(e))) ∈ (A List) supposing ↑e ∈b Buffer(n;X)
BY
{ (Auto THEN (RWO "is-interface-buffer" (-1) THENA Auto)) }

1
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)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    Buffer(n;X)(e)  =  lastn(n;X(\mleq{}(X)(e)))  supposing  \muparrow{}e  \mmember{}\msubb{}  Buffer(n;X)


By

---

Latex:
(Auto  THEN  (RWO  "is-interface-buffer"  (-1)  THENA  Auto))

---

Home Index