---

Step * of Lemma member-es-interface-history

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[A:Type]
      ∀X:EClass(A List). ∀e:E. ∀a:A.
        ((a ∈ es-interface-history(es;X;e)) ⇐⇒ ∃e':E. (((↑e' ∈b X) ∧ e' ≤loc e ) ∧ (a ∈ X(e'))))
BY
{ ((UnivCD
    THENM Unfold `es-interface-history` 0
    THENM RWO "member-concat" 0
    THENM RWO "member-mapfilter" 0
    THENM Reduce 0
    THENM RWO "member-es-le-before2" 0)
   THENA (All Reduce 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
⊢ ∃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')))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A:Type]
            \mforall{}X:EClass(A  List).  \mforall{}e:E.  \mforall{}a:A.
                ((a  \mmember{}  es-interface-history(es;X;e))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (((\muparrow{}e'  \mmember{}\msubb{}  X)  \mwedge{}  e'  \mleq{}loc  e  )  \mwedge{}  (a  \mmember{}  X(e'))))


By

---

Latex:
((UnivCD
    THENM  Unfold  `es-interface-history`  0
    THENM  RWO  "member-concat"  0
    THENM  RWO  "member-mapfilter"  0
    THENM  Reduce  0
    THENM  RWO  "member-es-le-before2"  0)
  THENA  (All  Reduce  THEN  Auto)
  )

---

Home Index