---

Step * of Lemma decidable__bag-member2

∀[T:Type]. ∀x:T. ((∀y:T. Dec(x = y ∈ T)) ⇒ (∀bs:bag(T). Dec(x ↓∈ bs)))
BY
{ xxx((UnivCD THENA Auto)
      THEN RenameVar `f' (-2)
      THEN (Assert ⌜Dec(↑bag-null([z∈bs|isl(f z)]))⌝⋅ THENA (Unfold `decidable` (-2) THEN Auto))
      THEN D (-1)
      THEN Unfold `decidable` 0)xxx }

1
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)

2
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)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  ((\mforall{}y:T.  Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}bs:bag(T).  Dec(x  \mdownarrow{}\mmember{}  bs)))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  RenameVar  `f'  (-2)
        THEN  (Assert  \mkleeneopen{}Dec(\muparrow{}bag-null([z\mmember{}bs|isl(f  z)]))\mkleeneclose{}\mcdot{}  THENA  (Unfold  `decidable`  (-2)  THEN  Auto))
        THEN  D  (-1)
        THEN  Unfold  `decidable`  0)xxx

---

Home Index