---

Step * of Lemma es-causl-total

∀es:EO. ∀e,e':E.  (e = e' ∈ E) ∨ (e < e') ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id
BY
{ (InstLemma `es-causl-total-base` [] THEN RepeatFor 5 (ParallelLast')) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e) = loc(e') ∈ Id
5. e = e' ∈ es-base-E(es)
⊢ e = e' ∈ E

---

Latex:


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


By

(InstLemma  `es-causl-total-base`  []  THEN  RepeatFor  5  (ParallelLast'))

---

Home Index