---

Step * of Lemma only_value_of_sv_class_in_classrel

∀[Info,T:Type].
  ∀eo:EO+(Info). ∀[e:E]. ∀[v:T]. ∀[X:EClass(T)].  ((v ∈ X(e) ∧ Singlevalued(X)) ⇒ (v = only(X eo e) ∈ T))
BY
{ ((UnivCD THENA Auto)
   THEN (FLemma `event_in_sv_classrel_is_in_class` [-1] THENA Auto)
   THEN (InstLemma `es-E-interface-property` [⌜Info⌝; ⌜eo⌝; ⌜X⌝; ⌜e⌝]⋅ THENA Auto)
   THEN RepUR ``in-eclass`` (-1)
   THEN D (-3)
   THEN RepUR ``classrel`` (-4)
   THEN (FLemma `assert_of_eq_int` [-1] THENA Auto)
   THEN (FLemma `bag-size-one` [-1] THENA Auto)
   THEN HypSubst' (-1 ) (-6)
   THEN FLemma `bag-member-single` [-6]
   THEN Auto) }

1
1. Info : Type
2. T : Type
3. eo : EO+(Info)@i'
4. e : E
5. v : T
6. X : EClass(T)
7. v ↓∈ {only(X eo e)}@i'
8. Singlevalued(X)@i'
9. e ∈ E(X)
10. ↑(#(X eo e) =z 1)
11. #(X eo e) = 1 ∈ ℤ
12. X eo e ~ {only(X eo e)}
⊢ single-valued-bag(X eo e;T)

---

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{}  (v  =  only(X  eo  e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (FLemma  `event\_in\_sv\_classrel\_is\_in\_class`  [-1]  THENA  Auto)
  THEN  (InstLemma  `es-E-interface-property`  [\mkleeneopen{}Info\mkleeneclose{};  \mkleeneopen{}eo\mkleeneclose{};  \mkleeneopen{}X\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``in-eclass``  (-1)
  THEN  D  (-3)
  THEN  RepUR  ``classrel``  (-4)
  THEN  (FLemma  `assert\_of\_eq\_int`  [-1]  THENA  Auto)
  THEN  (FLemma  `bag-size-one`  [-1]  THENA  Auto)
  THEN  HypSubst'  (-1  )  (-6)
  THEN  FLemma  `bag-member-single`  [-6]
  THEN  Auto)

---

Home Index