Step * of Lemma eo-reset-dom_wf

[es:EO]. ∀[d:es-base-E(es) ─→ 𝔹].  (eo-reset-dom(es;d) ∈ EO)
BY
(Auto⋅ THEN THEN MemTypeCD THEN Auto) }

1
1. es eo_record{i:l}()
2. eo_axioms(es)
3. es-base-E(es) ─→ 𝔹
⊢ eo-reset-dom(es;d) ∈ eo_record{i:l}()

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


Latex:


\mforall{}[es:EO].  \mforall{}[d:es-base-E(es)  {}\mrightarrow{}  \mBbbB{}].    (eo-reset-dom(es;d)  \mmember{}  EO)


By

(Auto\mcdot{}  THEN  D  1  THEN  MemTypeCD  THEN  Auto)




Home Index