---

Step * of Lemma not-tree-big

∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
  ((∃k:ℕ. T ~ ℕk)
  ⇒ Decidable(A)
  ⇒ (∀n:ℕ. ((¬tree-big(T;upwd-closure(T;A);n)) ⇒ (∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as)))))))
BY
{ Auto }

1
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. ∃k:ℕ. T ~ ℕk@i
4. Decidable(A)@i
5. n : ℕ@i
6. ¬tree-big(T;upwd-closure(T;A);n)@i
⊢ ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as)))

---

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{}
                ((\mneg{}tree-big(T;upwd-closure(T;A);n))
                {}\mRightarrow{}  (\mexists{}as:T  List.  ((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;A)  as)))))))


By

---

Latex:
Auto

---

Home Index