---

Step * of Lemma is-interface-left

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top + Top)]. ∀[e:E].  uiff(↑e ∈b left(X);(↑e ∈b X) ∧ (↑isl(X(e))))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``in-eclass es-interface-left eclass-val`` 0
   THEN RepUR ``eclass-compose1`` 0
   THEN GenConclAtAddr [2;1;1;1;1]
   THEN AutoSplit) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top + Top)
4. e : E
5. v : bag(Top + Top)@i
6. (X es e) = v ∈ bag(Top + Top)@i
7. #(v) = 1 ∈ ℤ
⊢ uiff(↑(#(fst(bag-separate(v))) =z 1);True ∧ (↑isl(only(v))))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top  +  Top)].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  left(X);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}isl(X(e))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``in-eclass  es-interface-left  eclass-val``  0
  THEN  RepUR  ``eclass-compose1``  0
  THEN  GenConclAtAddr  [2;1;1;1;1]
  THEN  AutoSplit)

---

Home Index