---

Step * 1 of Lemma assert-es-locless


1. es : EO@i'
2. ∀[e:es-base-E(es)]. (loc(e) ∈ Id)
⊢ ∀x,y:es-base-E(es).  ↑es-locless(es;x;y) ⇐⇒ (x < y) supposing loc(x) = loc(y) ∈ Id
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `es-loc-wf-base` [⌈es⌉;⌈x⌉]⋅ THENA Auto)
   THEN (InstLemma `es-loc-wf-base` [⌈es⌉;⌈y⌉]⋅ THENA Auto)
   THEN (InstLemma `es-locless-wf-base` [⌈es⌉]⋅ THENA Auto)
   THEN (InstLemma `es-causl-wf-base` [⌈es⌉]⋅ THENA Auto)
   THEN (D 0 THENA Auto)) }

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

---

Latex:



1.  es  :  EO@i'
2.  \mforall{}[e:es-base-E(es)].  (loc(e)  \mmember{}  Id)
\mvdash{}  \mforall{}x,y:es-base-E(es).    \muparrow{}es-locless(es;x;y)  \mLeftarrow{}{}\mRightarrow{}  (x  <  y)  supposing  loc(x)  =  loc(y)


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index