---

Step * 1 of Lemma assert-es-bless


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')
BY
{ (Decide ⌈loc(e) = loc(e') ∈ Id⌉⋅ THEN Try (Complete (Auto))) }

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

---

Latex:



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


By

(Decide  \mkleeneopen{}loc(e)  =  loc(e')\mkleeneclose{}\mcdot{}  THEN  Try  (Complete  (Auto)))

---

Home Index