---

Step * 1 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
{ xxx((OrRight THENA Auto)
      THEN (D 0 THENA Auto)
      THEN (InstLemma `bag-filter-empty` [⌜T⌝;⌜λz.isl(f z)⌝;⌜bs⌝;⌜x⌝]⋅
            THENA (Unfold `decidable` 3 THEN RepUR ``so_apply`` 0 THEN Auto)
            )
      THEN RepUR ``so_apply`` (-1)
      THEN D (-1)
      THEN Unfold `decidable` 3
      THEN (xxxGenConclTerm ⌜f x⌝⋅xxx THEN Auto)
      THEN (D (-2) THEN Auto)
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:

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


By

---

Latex:
xxx((OrRight  THENA  Auto)
        THEN  (D  0  THENA  Auto)
        THEN  (InstLemma  `bag-filter-empty`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}z.isl(f  z)\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
                    THENA  (Unfold  `decidable`  3  THEN  RepUR  ``so\_apply``  0  THEN  Auto)
                    )
        THEN  RepUR  ``so\_apply``  (-1)
        THEN  D  (-1)
        THEN  Unfold  `decidable`  3
        THEN  (xxxGenConclTerm  \mkleeneopen{}f  x\mkleeneclose{}\mcdot{}xxx  THEN  Auto)
        THEN  (D  (-2)  THEN  Auto)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index