---

Step * of Lemma assert-member-eclass

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  (↑e ∈b X ⇐⇒ ↓∃v:T. v ∈ X(e))
BY
{ ((UnivCD THENA Auto)
   THEN Unfolds ``member-eclass classrel`` 0
   THEN ((RW assert_pushdownC 0 THENA Auto) THEN (GenConclTerm ⌈X es e⌉⋅ THENA Auto))
   THEN skip{(RWO "bag-member-iff-size" 0 THEN Auto THEN Auto')}) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. v : bag(T)@i
7. (X es e) = v ∈ bag(T)@i
⊢ ¬(#(v) = 0 ∈ ℤ) ⇐⇒ ↓∃v@0:T. v@0 ↓∈ v

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))


By

((UnivCD  THENA  Auto)
  THEN  Unfolds  ``member-eclass  classrel``  0
  THEN  ((RW  assert\_pushdownC  0  THENA  Auto)  THEN  (GenConclTerm  \mkleeneopen{}X  es  e\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  skip\{(RWO  "bag-member-iff-size"  0  THEN  Auto  THEN  Auto')\})

---

Home Index