---

Step * 2 of Lemma decidable__bag-member2


1. [T] : Type
2. x : T
3. f : ∀y:T. Dec(x = y ∈ T)
4. bs : bag(T)
5. ¬↑bag-null([z∈bs|isl(f z)])
⊢ x ↓∈ bs ∨ (¬x ↓∈ bs)
BY
{ ((OrLeft THENA Auto)
   THEN Unfold `decidable` 3
   THEN (BagToList (-2) THENA Auto)
   THEN RepUR ``bag-null bag-filter`` (-1)
   THEN (BLemma `list-member-bag-member` THENA Auto)
   THEN (RWO "assert_of_null" (-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 ((Assert ⌜x = x1 ∈ T⌝⋅ THENM Auto)
         THEN (MoveToConcl (-1) THEN (xxxGenConclTerm ⌜f x1⌝⋅xxx THEN Auto) THEN D (-3) THEN Reduce (-1) THEN Trivial)⋅
         )⋅) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T
3.  f  :  \mforall{}y:T.  Dec(x  =  y)
4.  bs  :  bag(T)
5.  \mneg{}\muparrow{}bag-null([z\mmember{}bs|isl(f  z)])
\mvdash{}  x  \mdownarrow{}\mmember{}  bs  \mvee{}  (\mneg{}x  \mdownarrow{}\mmember{}  bs)


By

---

Latex:
((OrLeft  THENA  Auto)
  THEN  Unfold  `decidable`  3
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  RepUR  ``bag-null  bag-filter``  (-1)
  THEN  (BLemma  `list-member-bag-member`  THENA  Auto)
  THEN  (RWO  "assert\_of\_null"  (-1)  THENA  Auto)
  THEN  (FLemma  `member\_exists`  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "member\_filter"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RepD\mcdot{}
  THEN  ((Assert  \mkleeneopen{}x  =  x1\mkleeneclose{}\mcdot{}  THENM  Auto)
              THEN  (MoveToConcl  (-1)
                          THEN  (xxxGenConclTerm  \mkleeneopen{}f  x1\mkleeneclose{}\mcdot{}xxx  THEN  Auto)
                          THEN  D  (-3)
                          THEN  Reduce  (-1)
                          THEN  Trivial)\mcdot{}
              )\mcdot{})

---

Home Index