---

Step * of Lemma decidable__all_fun

∀[A,B:Type]. ∀[P:(A ⟶ B) ⟶ ℙ].  ((∃a:ℕ. A ~ ℕa) ⇒ (∃b:ℕ. B ~ ℕb) ⇒ (∀f:A ⟶ B. Dec(P[f])) ⇒ Dec(∀f:A ⟶ B. P[f]))
BY
{ ((Auto THEN ExRepD)
   THEN InstLemma `decidable__all_finite` [⌜A ⟶ B⌝;⌜b^a⌝;⌜P⌝]⋅
   THEN Auto
   THEN (Assert A ⟶ B ~ ℕa ⟶ ℕb BY
               EAuto 1)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:(A  {}\mrightarrow{}  B)  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}a:\mBbbN{}.  A  \msim{}  \mBbbN{}a)  {}\mRightarrow{}  (\mexists{}b:\mBbbN{}.  B  \msim{}  \mBbbN{}b)  {}\mRightarrow{}  (\mforall{}f:A  {}\mrightarrow{}  B.  Dec(P[f]))  {}\mRightarrow{}  Dec(\mforall{}f:A  {}\mrightarrow{}  B.  P[f]))


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  InstLemma  `decidable\_\_all\_finite`  [\mkleeneopen{}A  {}\mrightarrow{}  B\mkleeneclose{};\mkleeneopen{}b\^{}a\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Assert  A  {}\mrightarrow{}  B  \msim{}  \mBbbN{}a  {}\mrightarrow{}  \mBbbN{}b  BY
                          EAuto  1)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index