---

Step * 1 1 of Lemma member-es-interface-history


1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. X : EClass(A List)@i'
5. e : E@i
6. a : A@i
7. e' : E@i
8. ↑e' ∈b X@i
9. e' ≤loc e @i
10. (a ∈ X(e'))@i
⊢ ∃l:A List. ((∃y:{a:E| loc(a) = loc(e) ∈ Id} . (y ≤loc e  ∧ ((↑y ∈b X) c∧ (l = X(y) ∈ (A List))))) ∧ (a ∈ l))
BY
{ (With ⌈X(e')⌉ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [A]  :  Type
4.  X  :  EClass(A  List)@i'
5.  e  :  E@i
6.  a  :  A@i
7.  e'  :  E@i
8.  \muparrow{}e'  \mmember{}\msubb{}  X@i
9.  e'  \mleq{}loc  e  @i
10.  (a  \mmember{}  X(e'))@i
\mvdash{}  \mexists{}l:A  List.  ((\mexists{}y:\{a:E|  loc(a)  =  loc(e)\}  .  (y  \mleq{}loc  e    \mwedge{}  ((\muparrow{}y  \mmember{}\msubb{}  X)  c\mwedge{}  (l  =  X(y)))))  \mwedge{}  (a  \mmember{}  l))


By

---

Latex:
(With  \mkleeneopen{}X(e')\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index