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