---

Step * 5 of Lemma pes-axioms


1. the_es : EO@i'
⊢ ∀e:E. (pred(e) <loc e) ∧ (∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))) supposing ¬↑first(e)
BY
{ (RepeatFor 2 ((D 0⋅ THENA Auto)) THEN (FLemma `es-pred_property` [-1] THENA Auto) THEN Auto THEN D 0 THEN Auto) }

1
1. the_es : EO@i'
2. e : E@i
3. ¬↑first(e)
4. loc(pred(e)) = loc(e) ∈ Id
5. (pred(e) < e)
6. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
7. (pred(e) <loc e)
8. e' : E@i
9. (pred(e) <loc e')@i
10. (e' <loc e)@i
⊢ False

---

Latex:



1.  the$_{es}$  :  EO@i'
\mvdash{}  \mforall{}e:E.  (pred(e)  <loc  e)  \mwedge{}  (\mforall{}e':E.  (\mneg{}((pred(e)  <loc  e')  \mwedge{}  (e'  <loc  e))))  supposing  \mneg{}\muparrow{}first(e)


By

(RepeatFor  2  ((D  0\mcdot{}  THENA  Auto))
  THEN  (FLemma  `es-pred\_property`  [-1]  THENA  Auto)
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index