---

Step * of Lemma eo-restrict_wf

∀[es:EO]. ∀[P:E ─→ 𝔹].  (eo-restrict(es;P) ∈ EO)
BY
{ (Auto
   THEN Unfold `eo-restrict` 0
   THEN Fold `eo-reset-dom` 0
   THEN Fold `es-dom` 0
   THEN Unfold `es-E` -1
   THEN Folds ``es-base-E es-dom`` (-1)) }

1
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

---

Latex:


\mforall{}[es:EO].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbB{}].    (eo-restrict(es;P)  \mmember{}  EO)


By

(Auto
  THEN  Unfold  `eo-restrict`  0
  THEN  Fold  `eo-reset-dom`  0
  THEN  Fold  `es-dom`  0
  THEN  Unfold  `es-E`  -1
  THEN  Folds  ``es-base-E  es-dom``  (-1))

---

Home Index