---

Step * 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
⊢ False
BY
{ (Assert (e' ∈ s@i) BY
         Auto)⋅ }

1
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

---

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
\mvdash{}  False


By

(Assert  (e'  \mmember{}  s@i)  BY
              Auto)\mcdot{}

---

Home Index