---

Step * 1 of Lemma es-causal-antireflexive


1. the_es : EO
2. e : es-base-E(the_es)
3. ∀[e,e':es-base-E(the_es)].  ((e < e') ∈ ℙ)
4. (e < e)@i
5. es-rank(the_es;e) ∈ ℕ
⊢ False
BY
{ (InstLemma `es-rank_property-base` [⌈the_es⌉;⌈e⌉;⌈e⌉]⋅ THEN Auto) }

---

Latex:



1.  the$_{es}$  :  EO
2.  e  :  es-base-E(the$_{es}$)
3.  \mforall{}[e,e':es-base-E(the$_{es}$)].    ((e  <  e')  \mmember{}  \mBbbP{})
4.  (e  <  e)@i
5.  es-rank(the$_{es}$;e)  \mmember{}  \mBbbN{}
\mvdash{}  False


By

(InstLemma  `es-rank\_property-base`  [\mkleeneopen{}the$_{es}$\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index