Step
*
2
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@i
7. (a < b)@i
⊢ eo.e ∈ EO
BY
{ (BLemma `eo-forward-wf` THEN Auto)⋅ }
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)@i
7. (a < b)@i
\mvdash{} eo.e \mmember{} EO
By
(BLemma `eo-forward-wf` THEN Auto)\mcdot{}
Home
Index