---

Step * 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
⊢ ∃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))
⇐⇒ ∃e':E. (((↑e' ∈b X) ∧ e' ≤loc e ) ∧ (a ∈ X(e')))
BY
{ (Auto THEN ExRepD THEN Auto) }

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

---

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
\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))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (((\muparrow{}e'  \mmember{}\msubb{}  X)  \mwedge{}  e'  \mleq{}loc  e  )  \mwedge{}  (a  \mmember{}  X(e')))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  Auto)

---

Home Index