---

Step * of Lemma assert-es-ble-base

∀es:EO. ∀e,e':es-base-E(es).  (↑e ≤loc e' ⇐⇒ ((loc(e) = loc(e') ∈ Id) ∧ (e < e')) ∨ (e = e' ∈ es-base-E(es)))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``es-ble es-bless es-blocl`` 0) }

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

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':es-base-E(es).    (\muparrow{}e  \mleq{}loc  e'  \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  loc(e'))  \mwedge{}  (e  <  e'))  \mvee{}  (e  =  e'))


By

((UnivCD  THENA  Auto)  THEN  RepUR  ``es-ble  es-bless  es-blocl``  0)

---

Home Index