---

Step * 1 1 1 of Lemma es-fset-last_wf


1. es : EO
2. s : fset(E)
3. i : Id
4. ¬↑null(s@i)
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)
12. (last(s@i) <loc e')@i
13. last(s@i) ∈ s
14. loc(last(s@i)) = i ∈ Id
15. (e' ∈ s@i)
⊢ False
BY
{ (RepeatFor 2 (Thin (-2)) THEN RepeatFor 3 (MoveToConcl (-1)) THEN MoveToConcl (4)) }

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

---

Latex:

---

Latex:

1.  es  :  EO
2.  s  :  fset(E)
3.  i  :  Id
4.  \mneg{}\muparrow{}null(s@i)
5.  loc(s(i))  =  i
6.  s(i)  \mmember{}  s
7.  e'  :  E@i
8.  e'  \mmember{}  s@i
9.  \mforall{}e:E.  (e  \mmember{}  s  \mwedge{}  (loc(e)  =  i)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  s@i))
10.  no\_repeats(E;s@i)
11.  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;s@i)
12.  (last(s@i)  <loc  e')@i
13.  last(s@i)  \mmember{}  s
14.  loc(last(s@i))  =  i
15.  (e'  \mmember{}  s@i)
\mvdash{}  False


By

---

Latex:
(RepeatFor  2  (Thin  (-2))  THEN  RepeatFor  3  (MoveToConcl  (-1))  THEN  MoveToConcl  (4))

---

Home Index