---

Step * 1 of Lemma eo-restrict_wf


1. es : EO
2. P : {e:es-base-E(es)| ↑(es-dom(es) e)}  ─→ 𝔹
⊢ eo-reset-dom(es;λe.((es-dom(es) e) ∧b (P e))) ∈ EO
BY
{ Auto }

---

Latex:



1.  es  :  EO
2.  P  :  \{e:es-base-E(es)|  \muparrow{}(es-dom(es)  e)\}    {}\mrightarrow{}  \mBbbB{}
\mvdash{}  eo-reset-dom(es;\mlambda{}e.((es-dom(es)  e)  \mwedge{}\msubb{}  (P  e)))  \mmember{}  EO


By

Auto

---

Home Index