---

Step * 1 of Lemma not-tree-big


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)))
BY
{ Assert ⌜Dec(∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as))))⌝⋅ }

1
.....assertion..... 
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
⊢ Dec(∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as))))

2
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
7. Dec(∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as))))
⊢ ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k@i
4.  Decidable(A)@i
5.  n  :  \mBbbN{}@i
6.  \mneg{}tree-big(T;upwd-closure(T;A);n)@i
\mvdash{}  \mexists{}as:T  List.  ((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;A)  as)))


By

---

Latex:
Assert  \mkleeneopen{}Dec(\mexists{}as:T  List.  ((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;A)  as))))\mkleeneclose{}\mcdot{}

---

Home Index