---

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


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

1
1. es : EO@i'
2. e : es-base-E(es)@i
3. e' : es-base-E(es)@i
4. ∀[e:es-base-E(es)]. (loc(e) ∈ Id)
5. (e < e') ∈ ℙ
6. es-locless(es;e;e') ∈ 𝔹
7. e = e' ∈ 𝔹
⊢ ↑((es-locless(es;e;e') ∧b loc(e) = loc(e')) ∨be = e')
⇐⇒ ((loc(e) = loc(e') ∈ Id) ∧ (e < e')) ∨ (e = e' ∈ es-base-E(es))

---

Latex:



1.  es  :  EO@i'
2.  e  :  es-base-E(es)@i
3.  e'  :  es-base-E(es)@i
\mvdash{}  \muparrow{}((es-locless(es;e;e')  \mwedge{}\msubb{}  loc(e)  =  loc(e'))  \mvee{}\msubb{}e  =  e')
\mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  loc(e'))  \mwedge{}  (e  <  e'))  \mvee{}  (e  =  e')


By

((InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (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))

---

Home Index