---

Step * 1 2 1 of Lemma es-fset-at-loc


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)
6. L : {e:E| loc(e) = i ∈ Id}  List
7. ∀x:{e:E| loc(e) = i ∈ Id} . (x ∈ {e ∈ s | loc(e) = i} ⇐⇒ (x ∈ L))
8. ∃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))
BY
{ (ParallelLast 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)
6. L : {e:E| loc(e) = i ∈ Id}  List
7. ∀x:{e:E| loc(e) = i ∈ Id} . (x ∈ {e ∈ s | loc(e) = i} ⇐⇒ (x ∈ L))
8. L' : {e:E| loc(e) = i ∈ Id}  List
9. sorted-by(λe,e'. e ≤loc e' ;L')
10. no_repeats({e:E| loc(e) = i ∈ Id} ;L')
11. L ⊆ L'
12. L' ⊆ L
13. e : E@i
14. e ∈ s@i
15. loc(e) = i ∈ Id@i
⊢ (e ∈ L')

2
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)
6. L : {e:E| loc(e) = i ∈ Id}  List
7. ∀x:{e:E| loc(e) = i ∈ Id} . (x ∈ {e ∈ s | loc(e) = i} ⇐⇒ (x ∈ L))
8. L' : {e:E| loc(e) = i ∈ Id}  List
9. sorted-by(λe,e'. e ≤loc e' ;L')
10. no_repeats({e:E| loc(e) = i ∈ Id} ;L')
11. L ⊆ L'
12. L' ⊆ L
13. e : E@i
14. (e ∈ L')@i
⊢ e ∈ s

3
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)
6. L : {e:E| loc(e) = i ∈ Id}  List
7. ∀x:{e:E| loc(e) = i ∈ Id} . (x ∈ {e ∈ s | loc(e) = i} ⇐⇒ (x ∈ L))
8. L' : {e:E| loc(e) = i ∈ Id}  List
9. sorted-by(λe,e'. e ≤loc e' ;L')
10. no_repeats({e:E| loc(e) = i ∈ Id} ;L')
11. L ⊆ L'
12. L' ⊆ L
13. e : E@i
14. (e ∈ L')@i
⊢ loc(e) = i ∈ Id

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  i  :  Id@i
3.  s  :  fset(E)@i
4.  \mforall{}s:fset(\{e:E|  loc(e)  =  i\}  ).  \mexists{}L:\{e:E|  loc(e)  =  i\}    List.  \mforall{}x:\{e:E|  loc(e)  =  i\}  .  (x  \mmember{}  s  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L\000C))
5.  \mforall{}L:\{e:E|  loc(e)  =  i\}    List
          \mexists{}L':\{e:E|  loc(e)  =  i\}    List
            (sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;L')  \mwedge{}  no\_repeats(\{e:E|  loc(e)  =  i\}  ;L')  \mwedge{}  L  \msubseteq{}  L'  \mwedge{}  L'  \msubseteq{}  L)
6.  L  :  \{e:E|  loc(e)  =  i\}    List
7.  \mforall{}x:\{e:E|  loc(e)  =  i\}  .  (x  \mmember{}  \{e  \mmember{}  s  |  loc(e)  =  i\}  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))
8.  \mexists{}L':\{e:E|  loc(e)  =  i\}    List
        (sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;L')  \mwedge{}  no\_repeats(\{e:E|  loc(e)  =  i\}  ;L')  \mwedge{}  L  \msubseteq{}  L'  \mwedge{}  L'  \msubseteq{}  L)
\mvdash{}  \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

---

Latex:
(ParallelLast  THEN  Auto)

---

Home Index