---

Step * of Lemma event_in_sv_classrel_is_in_class

∀[Info,T:Type].  ∀eo:EO+(Info). ∀[e:E]. ∀[v:T]. ∀[X:EClass(T)].  ((v ∈ X(e) ∧ Singlevalued(X)) ⇒ (e ∈ E(X)))
BY
{ ((UnivCD THENA MaAuto)
   THEN D (-1)
   THEN RepUR ``es-E-interface in-eclass`` 0
   THEN RepUR ``classrel`` (-2)
   THEN RepUR ``sv-class`` (-1)
   THEN (InstHyp [⌜eo⌝; ⌜e⌝] (-1)⋅ THENA Auto)
   THEN MemTypeCD
   THEN Try (Complete (Auto))
   THEN (Assert ⌜(#(X eo e) = 0 ∈ ℤ) ∨ (#(X eo e) = 1 ∈ ℤ)⌝⋅ THENA Auto')
   THEN D (-1)
   THEN HypSubst' (-1) 0
   THEN HypSubst' (-1) (-2)
   THEN Auto
   THEN (InstLemma `bag-size-zero` [⌜T⌝; ⌜X eo e⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) (-5)
   THEN Try (Fold `empty-bag` (-5))
   THEN FLemma `bag-member-empty` [-5]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].
    \mforall{}eo:EO+(Info).  \mforall{}[e:E].  \mforall{}[v:T].  \mforall{}[X:EClass(T)].    ((v  \mmember{}  X(e)  \mwedge{}  Singlevalued(X))  {}\mRightarrow{}  (e  \mmember{}  E(X)))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  D  (-1)
  THEN  RepUR  ``es-E-interface  in-eclass``  0
  THEN  RepUR  ``classrel``  (-2)
  THEN  RepUR  ``sv-class``  (-1)
  THEN  (InstHyp  [\mkleeneopen{}eo\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  (Assert  \mkleeneopen{}(\#(X  eo  e)  =  0)  \mvee{}  (\#(X  eo  e)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  D  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  HypSubst'  (-1)  (-2)
  THEN  Auto
  THEN  (InstLemma  `bag-size-zero`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}X  eo  e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  (-5)
  THEN  Try  (Fold  `empty-bag`  (-5))
  THEN  FLemma  `bag-member-empty`  [-5]
  THEN  Auto)

---

Home Index