---

Step * 1 of Lemma eo-forward-le


1. eo : EO@i'
2. e : E@i
3. a : E@i
4. b : E@i
5. E ⊆r E
6. ((loc(a) = loc(b) ∈ Id) ∧ (a < b)) ∨ (a = b ∈ E)@i
⊢ ((loc(a) = loc(b) ∈ Id) ∧ (a < b)) ∨ (a = b ∈ E)
BY
{ ParallelLast }

1
1. eo : EO@i'
2. e : E@i
3. a : E@i
4. b : E@i
5. E ⊆r E
6. a = b ∈ E@i
⊢ a = b ∈ E

---

Latex:



1.  eo  :  EO@i'
2.  e  :  E@i
3.  a  :  E@i
4.  b  :  E@i
5.  E  \msubseteq{}r  E
6.  ((loc(a)  =  loc(b))  \mwedge{}  (a  <  b))  \mvee{}  (a  =  b)@i
\mvdash{}  ((loc(a)  =  loc(b))  \mwedge{}  (a  <  b))  \mvee{}  (a  =  b)


By

ParallelLast

---

Home Index