---

Step * of Lemma eo-restrict-restrict

∀[es:EO]. ∀[P:E ─→ 𝔹]. ∀[Q:{e:E| ↑(P e)}  ─→ 𝔹].
  (eo-restrict(eo-restrict(es;P);Q) = eo-restrict(es;λe.((P e) ∧b (Q e))) ∈ EO)
BY
{ (Auto THEN Unfold `eo-restrict` 0 THEN Reduce 0) }

1
1. es : EO
2. P : E ─→ 𝔹
3. Q : {e:E| ↑(P e)}  ─→ 𝔹
⊢ es["dom" := λe.((es."dom" e) ∧b (P e))]["dom" := λe.(((es."dom" e) ∧b (P e)) ∧b (Q e))]
= es["dom" := λe.((es."dom" e) ∧b (P e) ∧b (Q e))]
∈ EO

---

Latex:


\mforall{}[es:EO].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[Q:\{e:E|  \muparrow{}(P  e)\}    {}\mrightarrow{}  \mBbbB{}].
    (eo-restrict(eo-restrict(es;P);Q)  =  eo-restrict(es;\mlambda{}e.((P  e)  \mwedge{}\msubb{}  (Q  e))))


By

(Auto  THEN  Unfold  `eo-restrict`  0  THEN  Reduce  0)

---

Home Index