---

Step * of Lemma es-fset-at-loc

∀es:EO. ∀i:Id. ∀s:fset(E).
  ∃L:E List. ((∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ L))) ∧ no_repeats(E;L) ∧ sorted-by(λe,e'. e ≤loc e' ;L))
BY
{ (Auto
   THEN (InstLemma `fset-to-list` [⌈{e:E| loc(e) = i ∈ Id} ⌉;⌈es-eq(es)⌉;⌈λe,e'. e ≤loc e' ⌉]⋅
         THENA (Auto THEN Reduce 0 THEN Auto THEN BLemma `es-le-linorder` THEN Auto)
         )
   THEN (InstLemma `sorted-by-exists2` [⌈{e:E| loc(e) = i ∈ Id} ⌉;⌈λe,e'. e ≤loc e' ⌉]⋅
         THENA (Auto THEN Reduce 0 THEN Auto THEN Try ((BLemma `es-le-linorder` THEN Auto)))
         )) }

1
1. es : EO@i'
2. i : Id@i
3. s : fset(E)@i
4. ∀s:fset({e:E| loc(e) = i ∈ Id} ). ∃L:{e:E| loc(e) = i ∈ Id}  List. ∀x:{e:E| loc(e) = i ∈ Id} . (x ∈ s ⇐⇒ (x ∈ L))
5. ∀L:{e:E| loc(e) = i ∈ Id}  List
     ∃L':{e:E| loc(e) = i ∈ Id}  List. (sorted-by(λe,e'. e ≤loc e' ;L') ∧ no_repeats({e:E| loc(e) = i ∈ Id} ;L') ∧ L ⊆ L\000C' ∧ L' ⊆ L)
⊢ ∃L:E List. ((∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ L))) ∧ no_repeats(E;L) ∧ sorted-by(λe,e'. e ≤loc e' ;L))

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.  \mforall{}s:fset(E).
    \mexists{}L:E  List
      ((\mforall{}e:E.  (e  \mmember{}  s  \mwedge{}  (loc(e)  =  i)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  L)))  \mwedge{}  no\_repeats(E;L)  \mwedge{}  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;L))


By

(Auto
  THEN  (InstLemma  `fset-to-list`  [\mkleeneopen{}\{e:E|  loc(e)  =  i\}  \mkleeneclose{};\mkleeneopen{}es-eq(es)\mkleeneclose{};\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Reduce  0  THEN  Auto  THEN  BLemma  `es-le-linorder`  THEN  Auto)
              )
  THEN  (InstLemma  `sorted-by-exists2`  [\mkleeneopen{}\{e:E|  loc(e)  =  i\}  \mkleeneclose{};\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Reduce  0  THEN  Auto  THEN  Try  ((BLemma  `es-le-linorder`  THEN  Auto)))
              ))

---

Home Index