---

Step * 1 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
8. ||v|| - 1 ∈ ℕ||v||
⊢ False
BY
{ (D (-2) THEN (Decide i = (||v|| - 1) ∈ ℤ THENA 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. i : ℕ@i
8. i < ||v|| c∧ (e' = v[i] ∈ E)@i
9. ||v|| - 1 ∈ ℕ||v||
10. i = (||v|| - 1) ∈ ℤ
⊢ False

2
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. i : ℕ@i
8. i < ||v|| c∧ (e' = v[i] ∈ E)@i
9. ||v|| - 1 ∈ ℕ||v||
10. ¬(i = (||v|| - 1) ∈ ℤ)
⊢ 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
8.  ||v||  -  1  \mmember{}  \mBbbN{}||v||
\mvdash{}  False


By

---

Latex:
(D  (-2)  THEN  (Decide  i  =  (||v||  -  1)  THENA  Auto))

---

Home Index