---

Step * of Lemma same-loc-total

∀es:EO. ∀e,e':E.  (e < e') ∨ (e = e' ∈ E) ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id
BY
{ (InstLemma `es-locl-total` []
   THEN RepeatFor 3 (ParallelLast)
   THEN Auto
   THEN ThinTrivial
   THEN ParallelLast
   THEN Try (ParallelLast)
   THEN D -1
   THEN Auto) }

---

Latex:


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


By

(InstLemma  `es-locl-total`  []
  THEN  RepeatFor  3  (ParallelLast)
  THEN  Auto
  THEN  ThinTrivial
  THEN  ParallelLast
  THEN  Try  (ParallelLast)
  THEN  D  -1
  THEN  Auto)

---

Home Index