---

Step * of Lemma es-fset-last_wf

∀[es:EO]. ∀[s:fset(E)]. ∀[i:Id].
  s(i) ∈ {e:E| (loc(e) = i ∈ Id) ∧ e ∈ s ∧ (∀e':E. (e' ∈ s ⇒ (¬(e <loc e'))))}  supposing i ∈ locs(s)
BY
{ (Auto
   THEN MemTypeCD
   THEN Auto
   THEN ((Unfold `es-fset-last` 0 THEN Auto THEN Try (Complete ((UnfoldTopAb (-1) THEN Auto))))
         THEN InstLemma `es-fset-at-property` [⌈es⌉;⌈i⌉;⌈s⌉]⋅
         THEN Auto)⋅) }

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

---

Latex:


\mforall{}[es:EO].  \mforall{}[s:fset(E)].  \mforall{}[i:Id].
    s(i)  \mmember{}  \{e:E|  (loc(e)  =  i)  \mwedge{}  e  \mmember{}  s  \mwedge{}  (\mforall{}e':E.  (e'  \mmember{}  s  {}\mRightarrow{}  (\mneg{}(e  <loc  e'))))\}    supposing  i  \mmember{}  locs(s)


By

(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  ((Unfold  `es-fset-last`  0  THEN  Auto  THEN  Try  (Complete  ((UnfoldTopAb  (-1)  THEN  Auto))))
              THEN  InstLemma  `es-fset-at-property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index