---

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


1. es : EO@i'
2. e' : E@i
3. v : E List@i
4. ¬↑null(v)@i
5. sorted-by(λe,e'. e ≤loc e' ;v)@i
6. (last(v) <loc e')@i
7. (e' ∈ v)@i
⊢ False
BY
{ (Assert ||v|| - 1 ∈ ℕ||v|| BY
         ((DVar `v'⋅ THEN All Reduce) THEN Auto')) }

1
1. es : EO@i'
2. e' : E@i
3. v : E List@i
4. ¬↑null(v)@i
5. sorted-by(λe,e'. e ≤loc e' ;v)@i
6. (last(v) <loc e')@i
7. (e' ∈ v)@i
8. ||v|| - 1 ∈ ℕ||v||
⊢ False

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  e'  :  E@i
3.  v  :  E  List@i
4.  \mneg{}\muparrow{}null(v)@i
5.  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;v)@i
6.  (last(v)  <loc  e')@i
7.  (e'  \mmember{}  v)@i
\mvdash{}  False


By

---

Latex:
(Assert  ||v||  -  1  \mmember{}  \mBbbN{}||v||  BY
              ((DVar  `v'\mcdot{}  THEN  All  Reduce)  THEN  Auto'))

---

Home Index