---

Step * 1 2 of Lemma es-eq-wf-base


1. es : EO
⊢ ∀x,y:es-base-E(es).
    (x = y ∈ es-base-E(es) ⇐⇒ ↑(loc(x) = loc(y) ∧b (¬bes-locless(es;x;y)) ∧b (¬bes-locless(es;y;x))))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. es : EO
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
⊢ x = y ∈ es-base-E(es) ⇐⇒ ↑(loc(x) = loc(y) ∧b (¬bes-locless(es;x;y)) ∧b (¬bes-locless(es;y;x)))

---

Latex:



1.  es  :  EO
\mvdash{}  \mforall{}x,y:es-base-E(es).
        (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(loc(x)  =  loc(y)  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;x;y))  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;y;x))))


By

RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index