---

Step * of Lemma decidable__tree-big

∀[T:Type]. ∀[A:(T List) ⟶ ℙ].  ((∃k:ℕ. T ~ ℕk) ⇒ Decidable(A) ⇒ (∀n:ℕ. Dec(tree-big(T;A;n))))
BY
{ (RepUR ``tree-big dec-predicate`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:(T  List)  {}\mrightarrow{}  \mBbbP{}].    ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  Decidable(A)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  Dec(tree-big(T;A;n))))


By

---

Latex:
(RepUR  ``tree-big  dec-predicate``  0  THEN  Auto)

---

Home Index