---

Step * 1 of Lemma bag-count-member


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. 1 ≤ #([y∈b|eq x y])
⊢ x ↓∈ b
BY
{ ((Assert ⌜∀y:T. (x = y ∈ T ⇐⇒ ↑(eq x y))⌝⋅ THENA (D 2 THEN (Unhide THENA Auto) THEN InstHyp [⌜x⌝] 3⋅ THEN Auto))
   THEN RepUR ``bag-size bag-filter`` (-2)
   THEN (InstLemma `length_of_not_nil` [⌜T⌝;⌜filter(λy.(eq x y);b)⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN Thin (-2)
   THEN (D (-1) THENA Auto)
   THEN (FLemma `member_exists` [-1] THENA Auto)
   THEN ExRepD
   THEN (RWO "member_filter" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN RepD
   THEN (InstHyp [⌜x1⌝] (-5)⋅ THENA Auto)
   THEN (RWO "-1<" (-2) THENA Auto)
   THEN RWO "bag-member-list" 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  b  :  T  List
5.  1  \mleq{}  \#([y\mmember{}b|eq  x  y])
\mvdash{}  x  \mdownarrow{}\mmember{}  b


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}y:T.  (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(eq  x  y))\mkleeneclose{}\mcdot{}
    THENA  (D  2  THEN  (Unhide  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THEN  Auto)
    )
  THEN  RepUR  ``bag-size  bag-filter``  (-2)
  THEN  (InstLemma  `length\_of\_not\_nil`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}filter(\mlambda{}y.(eq  x  y);b)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Thin  (-2)
  THEN  (D  (-1)  THENA  Auto)
  THEN  (FLemma  `member\_exists`  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "member\_filter"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RepD
  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1<"  (-2)  THENA  Auto)
  THEN  RWO  "bag-member-list"  0
  THEN  Auto)\mcdot{}

---

Home Index