---

Step * of Lemma eo-reset-dom-reset-dom

∀[es:EO]. ∀[d1,d2:es-base-E(es) ─→ 𝔹].  (eo-reset-dom(eo-reset-dom(es;d1);d2) = eo-reset-dom(es;d2) ∈ EO)
BY
{ (Auto
   THEN Unfold `eo-reset-dom` 0
   THEN (RWO  "record-update-update" 0 THENA Auto)
   THEN Fold `eo-reset-dom` 0
   THEN Auto)⋅ }

---

Latex:


\mforall{}[es:EO].  \mforall{}[d1,d2:es-base-E(es)  {}\mrightarrow{}  \mBbbB{}].    (eo-reset-dom(eo-reset-dom(es;d1);d2)  =  eo-reset-dom(es;d2))


By

(Auto
  THEN  Unfold  `eo-reset-dom`  0
  THEN  (RWO    "record-update-update"  0  THENA  Auto)
  THEN  Fold  `eo-reset-dom`  0
  THEN  Auto)\mcdot{}

---

Home Index