---

Step * 1 of Lemma es-fset-last_wf


1. es : EO
2. s : fset(E)
3. i : Id
4. i ∈ locs(s)
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)
⊢ ¬(last(s@i) <loc e')
BY
{ (UnfoldTopAb 4
   THEN (D 0 THENA Auto)
   THEN (InstHyp[⌈last(s@i)⌉] 9⋅ THENA Auto)
   THEN D (-1)
   THEN Thin (-2)
   THEN D -1
   THEN 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
⊢ False

---

Latex:



1.  es  :  EO
2.  s  :  fset(E)
3.  i  :  Id
4.  i  \mmember{}  locs(s)
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)
\mvdash{}  \mneg{}(last(s@i)  <loc  e')


By

(UnfoldTopAb  4
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp[\mkleeneopen{}last(s@i)\mkleeneclose{}]  9\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Thin  (-2)
  THEN  D  -1
  THEN  Auto)

---

Home Index