---

Step * of Lemma es-causl-total-base

∀es:EO. ∀e,e':es-base-E(es).  (e = e' ∈ es-base-E(es)) ∨ (e < e') ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id
BY
{ (InstLemma `es-locless-property` []
   THEN ParallelLast
   THEN DupHyp (-1)
   THEN RepeatFor 2 (ParallelLast⋅)
   THEN (InstLemma `es-loc-wf-base` [⌈es⌉]⋅ THENA Auto)
   THEN ParallelOp -2
   THEN ((InstLemma `decidable__es-causl-same-loc` [⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THENA Auto)
         THEN (InstLemma `decidable__es-causl-same-loc` [⌈es⌉;⌈e'⌉;⌈e⌉]⋅ THENA Auto)
         )
   THEN ((InstLemma `es-causl-wf-base` [⌈es⌉]⋅ THENA Auto) THEN (InstLemma `es-locless-wf-base` [⌈es⌉]⋅ THENA Auto))
   THEN (D -4 THEN Auto)
   THEN D -3
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':es-base-E(es).    (e  =  e')  \mvee{}  (e  <  e')  \mvee{}  (e'  <  e)  supposing  loc(e)  =  loc(e')


By

(InstLemma  `es-locless-property`  []
  THEN  ParallelLast
  THEN  DupHyp  (-1)
  THEN  RepeatFor  2  (ParallelLast\mcdot{})
  THEN  (InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  ((InstLemma  `decidable\_\_es-causl-same-loc`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `decidable\_\_es-causl-same-loc`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  THEN  ((InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  THEN  (D  -4  THEN  Auto)
  THEN  D  -3
  THEN  Auto)

---

Home Index