---

Step * 1 of Lemma eo-restrict_wf_extended


1. Info : Type
2. es : EO+(Info)
3. P : E ─→ 𝔹
4. es ∈ EO
⊢ eo-restrict(es;P)."info" ∈ es-base-E(eo-restrict(es;P)) ─→ Info
BY
{ (Thin (-1) THEN (Unfold `eo-restrict` 0 THEN Reduce 0 THEN DRecord 2 ⋅ THEN Auto)⋅) }

1
1. Info : Type
2. es : self:EO ∩ x:Atom ─→ if x =a "info" then es-base-E(self) ─→ Info else Top fi 
3. es ∈ EO
4. P : E ─→ 𝔹
5. es."info" ∈ es-base-E(es) ─→ Info
⊢ es."info" ∈ es-base-E(es["dom" := λe.((es."dom" e) ∧b (P e))]) ─→ Info

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  P  :  E  {}\mrightarrow{}  \mBbbB{}
4.  es  \mmember{}  EO
\mvdash{}  eo-restrict(es;P)."info"  \mmember{}  es-base-E(eo-restrict(es;P))  {}\mrightarrow{}  Info


By

(Thin  (-1)  THEN  (Unfold  `eo-restrict`  0  THEN  Reduce  0  THEN  DRecord  2  \mcdot{}  THEN  Auto)\mcdot{})

---

Home Index