---

Step * 2 of Lemma eo-reset-dom_wf

.....set predicate..... 
1. es : eo_record{i:l}()
2. eo_axioms(es)
3. d : es-base-E(es) ─→ 𝔹
⊢ eo_axioms(eo-reset-dom(es;d))
BY
{ (ParallelOp -2 THEN RepUR ``eo-reset-dom`` 0 THEN Trivial) }

---

Latex:


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


By

(ParallelOp  -2  THEN  RepUR  ``eo-reset-dom``  0  THEN  Trivial)

---

Home Index