---

Step * of Lemma eo-forward-le2

∀eo:EO. ∀e:E. ∀a,b:E.  (a ≤loc b  ⇒ a ≤loc b )
BY
{ (InstLemma `eo-forward-le` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (InstLemma `eo-forward-wf` [⌈eo⌉;⌈e⌉]⋅ THENA Auto)
   THEN RepeatFor 3 ((D 0 THENA Auto))) }

1
1. eo : EO@i'
2. e : E@i
3. ∀a,b:E.  (a ≤loc b  ⇐⇒ a ≤loc b )
4. eo.e ∈ EO
5. a : E@i
6. b : E@i
7. a ≤loc b @i
⊢ a ≤loc b 

---

Latex:


\mforall{}eo:EO.  \mforall{}e:E.  \mforall{}a,b:E.    (a  \mleq{}loc  b    {}\mRightarrow{}  a  \mleq{}loc  b  )


By

(InstLemma  `eo-forward-le`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (InstLemma  `eo-forward-wf`  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  ((D  0  THENA  Auto)))

---

Home Index