---

Step * of Lemma decidable__exists_bag-member

∀[T:Type]. ∀b:bag(T). Dec(↓∃x:T. x ↓∈ b)
BY
{ (Auto
   THEN (Assert Dec(0 < #(b)) BY
               Auto)
   THEN Repeat (ParallelLast)
   THEN Try ((FLemma `bag-size-bag-member` [-1] THEN Auto))) }

---

Latex:


\mforall{}[T:Type].  \mforall{}b:bag(T).  Dec(\mdownarrow{}\mexists{}x:T.  x  \mdownarrow{}\mmember{}  b)


By

(Auto
  THEN  (Assert  Dec(0  <  \#(b))  BY
                          Auto)
  THEN  Repeat  (ParallelLast)
  THEN  Try  ((FLemma  `bag-size-bag-member`  [-1]  THEN  Auto)))

---

Home Index