---

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


1. es : EO
2. e : es-base-E(es)
3. e' : es-base-E(es)
⊢ (es-locless(es;e;e') ∧b loc(e) = loc(e')) ∨be = e' ∈ 𝔹
BY
{ (((InstLemma `es-locless-wf-base` [⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THENA Auto)
    THEN (InstLemma `es-eq-E-wf-base` [⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THENA Auto)
    )
   THEN InstLemma `es-loc-wf-base` [⌈es⌉]⋅
   THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  es-base-E(es)
3.  e'  :  es-base-E(es)
\mvdash{}  (es-locless(es;e;e')  \mwedge{}\msubb{}  loc(e)  =  loc(e'))  \mvee{}\msubb{}e  =  e'  \mmember{}  \mBbbB{}


By

(((InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (InstLemma  `es-eq-E-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
    )
  THEN  InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index