---

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


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
BY
{ (GenConclAtAddr [1;1;1;1] THEN Lemmaize[]) }

1
∀es:EO. ∀e':E. ∀v:E List.  ((¬↑null(v)) ⇒ sorted-by(λe,e'. e ≤loc e' ;v) ⇒ (last(v) <loc e') ⇒ (e' ∈ v) ⇒ False)

---

Latex:



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


By

(GenConclAtAddr  [1;1;1;1]  THEN  Lemmaize[])

---

Home Index