---

Step * of Lemma decidable__exists_classrel

∀[Info,T:Type].  ∀X:EClass(T). ∀es:EO+(Info). ∀e:E.  Dec(↓∃v:T. v ∈ X(e))
BY
{ ((Auto THEN Unfold `classrel` 0 THEN Auto)
   THEN (Assert Dec(0 < #(X es e)) BY
               Auto)
   THEN Repeat (ParallelLast)
   THEN Try ((FLemma `bag-size-bag-member` [-1] THEN Auto))) }

---

Latex:


\mforall{}[Info,T:Type].    \mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))


By

((Auto  THEN  Unfold  `classrel`  0  THEN  Auto)
  THEN  (Assert  Dec(0  <  \#(X  es  e))  BY
                          Auto)
  THEN  Repeat  (ParallelLast)
  THEN  Try  ((FLemma  `bag-size-bag-member`  [-1]  THEN  Auto)))

---

Home Index