---

Step * of Lemma es-fset-loc-iff

∀es:EO. ∀s:fset(E). ∀i:Id.  (i ∈ locs(s) ⇐⇒ ∃e:E. ((loc(e) = i ∈ Id) ∧ e ∈ s))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-fset-loc` 0
   THEN (InstLemma `es-fset-at-property` [⌜es⌝;⌜i⌝;⌜s⌝]⋅ THENA Auto)
   THEN (MoveToConcl  (-1) THEN GenConclAtAddr [2;1;1;1;1])
   THEN Auto) }

1
1. es : EO@i'
2. s : fset(E)@i
3. i : Id@i
4. v : E List@i
5. s@i = v ∈ (E List)@i
6. ∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ v))@i
7. no_repeats(E;v)@i
8. sorted-by(λe,e'. e ≤loc e' ;v)@i
9. ¬↑null(v)@i
⊢ ∃e:E. ((loc(e) = i ∈ Id) ∧ e ∈ s)

2
1. es : EO@i'
2. s : fset(E)@i
3. i : Id@i
4. v : E List@i
5. s@i = v ∈ (E List)@i
6. ∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ v))@i
7. no_repeats(E;v)@i
8. sorted-by(λe,e'. e ≤loc e' ;v)@i
9. ∃e:E. ((loc(e) = i ∈ Id) ∧ e ∈ s)@i
⊢ ¬↑null(v)

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}s:fset(E).  \mforall{}i:Id.    (i  \mmember{}  locs(s)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e:E.  ((loc(e)  =  i)  \mwedge{}  e  \mmember{}  s))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `es-fset-loc`  0
  THEN  (InstLemma  `es-fset-at-property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl    (-1)  THEN  GenConclAtAddr  [2;1;1;1;1])
  THEN  Auto)

---

Home Index