---

Step * 2 of Lemma bag-count-member


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. x ↓∈ b
⊢ 1 ≤ #([y∈b|eq x y])
BY
{ ((RWO "bag-member-list" (-1) THENA Auto)
   THEN RepUR ``bag-size bag-filter`` 0
   THEN (RWO "l_member_decomp" (-1) THENA Auto)
   THEN ExRepD
   THEN HypSubst' (-1) 0
   THEN ThinVar `b'
   THEN RepeatFor 2 ((RWO "filter_append" 0 THENA Auto))
   THEN RepeatFor 2 ((RWO "length_append" 0 THENA Auto))
   THEN Reduce 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0
   THEN Auto'
   THEN D (-1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "bag-member-list"  (-1)  THENA  Auto)
  THEN  RepUR  ``bag-size  bag-filter``  0
  THEN  (RWO  "l\_member\_decomp"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  ThinVar  `b'
  THEN  RepeatFor  2  ((RWO  "filter\_append"  0  THENA  Auto))
  THEN  RepeatFor  2  ((RWO  "length\_append"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto'
  THEN  D  (-1)
  THEN  Auto)\mcdot{}

---

Home Index