Step
*
2
2
of Lemma
eo-forward-trivial
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. ↑first(e)
5. (λx.((eo."dom" x) ∧b (e ≤loc x ∨b(¬bloc(x) = loc(e))))) = eo."dom" ∈ (es-base-E(eo) ─→ 𝔹)
6. z : es-base-E(eo) ─→ 𝔹
⊢ eo["dom" := z] ∈ EO+(Info)
BY
{ (Fold `eo-reset-dom` 0⋅ THEN Auto) }
Latex:
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. \muparrow{}first(e)
5. (\mlambda{}x.((eo."dom" x) \mwedge{}\msubb{} (e \mleq{}loc x \mvee{}\msubb{}(\mneg{}\msubb{}loc(x) = loc(e))))) = eo."dom"
6. z : es-base-E(eo) {}\mrightarrow{} \mBbbB{}
\mvdash{} eo["dom" := z] \mmember{} EO+(Info)
By
(Fold `eo-reset-dom` 0\mcdot{} THEN Auto)
Home
Index