---

Step * of Lemma assert-es-bless

∀es:EO. ∀e,e':E.  (↑e <loc e' ⇐⇒ (e <loc e'))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``es-bless es-blocl es-locl`` 0 THEN (RW assert_pushdownC 0 THENA Auto)) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
⊢ (↑es-locless(es;e;e')) ∧ (loc(e) = loc(e') ∈ Id) ⇐⇒ (loc(e) = loc(e') ∈ Id) ∧ (e < e')

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (\muparrow{}e  <loc  e'  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e'))


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-bless  es-blocl  es-locl``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index