---

Step * of Lemma eo-restrict_property

∀es:EO. ∀P:E ⟶ 𝔹.  (E ≡ {e:E| ↑(P e)}  ∧ (∀e:E. (loc(e) = loc(e) ∈ Id)) ∧ (∀e1,e2:E.  ((e1 < e2) ⇐⇒ (e1 < e2))))
BY
{ (Auto
   THEN (All (\h. (RepUR ``eo-restrict es-E es-base-E es-loc es-causl`` h
                   THEN Repeat (Folds
                                ``es-causl es-loc es-E`` h⋅)
                   ))⋅
         THEN Auto
         )⋅
   ) }

1
1. es : EO@i'
2. P : E ⟶ 𝔹@i
⊢ {e:es."E"| ↑((es."dom" e) ∧b (P e))}  ≡ {e:E| ↑(P e)} 

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}P:E  {}\mrightarrow{}  \mBbbB{}.
    (E  \mequiv{}  \{e:E|  \muparrow{}(P  e)\}    \mwedge{}  (\mforall{}e:E.  (loc(e)  =  loc(e)))  \mwedge{}  (\mforall{}e1,e2:E.    ((e1  <  e2)  \mLeftarrow{}{}\mRightarrow{}  (e1  <  e2))))


By

---

Latex:
(Auto
  THEN  (All  (\mbackslash{}h.  (RepUR  ``eo-restrict  es-E  es-base-E  es-loc  es-causl``  h
                                  THEN  Repeat  (Folds
                                                            ``es-causl  es-loc  es-E``  h\mcdot{})
                                  ))\mcdot{}
              THEN  Auto
              )\mcdot{}
  )

---

Home Index