---

Step * 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))
⊢ (∀e∈s@i.↑e ∈b X)
BY
{ ((BLemma `l_all_iff` THEN Auto)
   THEN ((InstLemma `es-fset-at-property` [⌈es⌉;⌈i⌉;⌈s⌉]⋅
         THENM (D -1 THEN (InstHyp [⌈e⌉] (-2)⋅ THENM (ThinTrivial THEN Auto)))
         )
         THENA Auto
         )
   ) }

1
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

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  i  :  Id
5.  s  :  fset(E(X))
\mvdash{}  (\mforall{}e\mmember{}s@i.\muparrow{}e  \mmember{}\msubb{}  X)


By

---

Latex:
((BLemma  `l\_all\_iff`  THEN  Auto)
  THEN  ((InstLemma  `es-fset-at-property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
              THENM  (D  -1  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}  THENM  (ThinTrivial  THEN  Auto)))
              )
              THENA  Auto
              )
  )

---

Home Index