---

Step * of Lemma l-exists-decider_wf

∀[A:Type]. ∀[F:A ⟶ ℙ].  ∀L:A List. ∀dcd:∀k:A. Dec(F[k]).  (l-exists-decider() L dcd ∈ Dec((∃k∈L. F[k])))
BY
{ (Auto
   THEN (Assert TERMOF{decidable__l_exists:o, \\v:l, i:l} ∈ ∀[A:Type]. ∀[F:A ⟶ ℙ].
                                                              ∀L:A List. ((∀k:A. Dec(F[k])) ⇒ Dec((∃k∈L. F[k]))) BY
               Auto)
   THEN RW (AddrC [2] (TagC (mk_tag_term 1))) (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[F:A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L:A  List.  \mforall{}dcd:\mforall{}k:A.  Dec(F[k]).    (l-exists-decider()  L  dcd  \mmember{}  Dec((\mexists{}k\mmember{}L.  F[k])))


By

---

Latex:
(Auto
  THEN  (Assert  TERMOF\{decidable\_\_l\_exists:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  \mmember{}  \mforall{}[A:Type].  \mforall{}[F:A  {}\mrightarrow{}  \mBbbP{}].
                                                                                                                        \mforall{}L:A  List
                                                                                                                            ((\mforall{}k:A.  Dec(F[k]))
                                                                                                                            {}\mRightarrow{}  Dec((\mexists{}k\mmember{}L.  F[k])))  BY
                          Auto)
  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  (-1)
  THEN  Auto)

---

Home Index