---

Step * of Lemma es-ble-wf-base

∀[es:EO]. ∀[e,e':es-base-E(es)].  (e ≤loc e' ∈ 𝔹)
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN RepUR ``es-ble es-bless es-blocl`` 0) }

1
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' ∈ 𝔹

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':es-base-E(es)].    (e  \mleq{}loc  e'  \mmember{}  \mBbbB{})


By

(RepeatFor  3  ((D  0  THENA  Auto))  THEN  RepUR  ``es-ble  es-bless  es-blocl``  0)

---

Home Index