---

Step * 1 of Lemma eo-reset-dom_wf


1. es : eo_record{i:l}()
2. eo_axioms(es)
3. d : es-base-E(es) ─→ 𝔹
⊢ eo-reset-dom(es;d) ∈ eo_record{i:l}()
BY
{ ((DRecord 1 THENA Auto)
   THEN Unfolds ``eo_record eo-reset-dom`` 0
   THEN RepeatFor 7 ((RecordPlusTypeCD THEN Try ((Reduce 0 THEN (Trivial ORELSE (Fold `es-base-E` 0 THEN Trivial))))))
   THEN Auto) }

---

Latex:



1.  es  :  eo\_record\{i:l\}()
2.  eo\_axioms(es)
3.  d  :  es-base-E(es)  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  eo-reset-dom(es;d)  \mmember{}  eo\_record\{i:l\}()


By

((DRecord  1  THENA  Auto)
  THEN  Unfolds  ``eo\_record  eo-reset-dom``  0
  THEN  RepeatFor  7  ((RecordPlusTypeCD
                                        THEN  Try  ((Reduce  0  THEN  (Trivial  ORELSE  (Fold  `es-base-E`  0  THEN  Trivial))))
                                        ))
  THEN  Auto)

---

Home Index