---

Step * of Lemma es-blocl-iff

∀es:EO. ∀e1,e2:E.  (↑es-blocl(es;e1;e2) ⇐⇒ (e1 <loc e2))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN Auto) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. ↑es-blocl(es;e1;e2)@i
⊢ (e1 <loc e2)

2
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. (e1 <loc e2)@i
⊢ ↑es-blocl(es;e1;e2)

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.    (\muparrow{}es-blocl(es;e1;e2)  \mLeftarrow{}{}\mRightarrow{}  (e1  <loc  e2))


By

((UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index