---

Step * 1 1 of Lemma bag-member-count


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. L : T List
5. (x ∈ L)
⊢ 1 ≤ ||filter(λy.(eq x y);L)||
BY
{ ((InstLemma `filter_is_empty` [⌜T⌝;λy.(eq x y);⌜L⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [2;2;1]
   THEN Auto
   THEN DVar `v'
   THEN All Reduce
   THEN Auto'
   THEN D -4
   THEN (InstHyp [⌜i⌝] (-2)⋅ THENA Auto)
   THEN D (-1)
   THEN RW assert_pushdownC 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  L  :  T  List
5.  (x  \mmember{}  L)
\mvdash{}  1  \mleq{}  ||filter(\mlambda{}y.(eq  x  y);L)||


By

---

Latex:
((InstLemma  `filter\_is\_empty`  [\mkleeneopen{}T\mkleeneclose{};\mlambda{}y.(eq  x  y);\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [2;2;1]
  THEN  Auto
  THEN  DVar  `v'
  THEN  All  Reduce
  THEN  Auto'
  THEN  D  -4
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index