---

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


1. es : EO
⊢ λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1))) ∈ EqDecider(es-base-E(es))
BY
{ (MemTypeCD THEN Reduce 0) }

1
1. es : EO
⊢ λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1))) ∈ es-base-E(es) ─→ es-base-E(es) ─\000C→ 𝔹

2
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))))

3
.....wf..... 
1. es : EO
2. eq : es-base-E(es) ─→ es-base-E(es) ─→ 𝔹
⊢ ∀x,y:es-base-E(es).  (x = y ∈ es-base-E(es) ⇐⇒ ↑(eq x y)) ∈ Type

---

Latex:



1.  es  :  EO
\mvdash{}  \mlambda{}e1,e2.  (loc(e1)  =  loc(e2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e1;e2))  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e2;e1)))
    \mmember{}  EqDecider(es-base-E(es))


By

(MemTypeCD  THEN  Reduce  0)

---

Home Index