---

Step * 1 1 of Lemma es-fset-at_wf-interface


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. i : Id
5. s : fset(E(X))
6. e : E@i
7. (e ∈ s@i)@i
8. ∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ s@i))
9. no_repeats(E;s@i)
10. sorted-by(λe,e'. e ≤loc e' ;s@i)
11. (e ∈ s ∧ (loc(e) = i ∈ Id)) ⇒ (e ∈ s@i)
12. e ∈ s
13. loc(e) = i ∈ Id
⊢ ↑e ∈b X
BY
{ ((Using [`A',⌈E(X)⌉] (FLemma `strong-subtype-fset-member-type`[-2])⋅ THENM MemTypeHD (-1)) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  i  :  Id
5.  s  :  fset(E(X))
6.  e  :  E@i
7.  (e  \mmember{}  s@i)@i
8.  \mforall{}e:E.  (e  \mmember{}  s  \mwedge{}  (loc(e)  =  i)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  s@i))
9.  no\_repeats(E;s@i)
10.  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;s@i)
11.  (e  \mmember{}  s  \mwedge{}  (loc(e)  =  i))  {}\mRightarrow{}  (e  \mmember{}  s@i)
12.  e  \mmember{}  s
13.  loc(e)  =  i
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  X


By

---

Latex:
((Using  [`A',\mkleeneopen{}E(X)\mkleeneclose{}]  (FLemma  `strong-subtype-fset-member-type`[-2])\mcdot{}  THENM  MemTypeHD  (-1))
  THEN  Auto
  )\mcdot{}

---

Home Index