---

Step * 2 of Lemma tree-big-least


1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. ∃k:ℕ. T ~ ℕk@i
4. Decidable(A)@i
5. ¬(A [])@i
6. n : ℤ@i
7. [%4] : 0 < n@i
8. tree-big(T;upwd-closure(T;A);n - 1)
⇒ (∃k:ℕn - 1. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1)))@i
9. tree-big(T;upwd-closure(T;A);n)@i
⊢ ∃k:ℕn. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1))
BY
{ ( Assert  ⌜Dec(tree-big(T;upwd-closure(T;A);n - 1))⌝⋅ THEN Auto) }

1
.....decidable?..... 
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. ∃k:ℕ. T ~ ℕk@i
4. Decidable(A)@i
5. ¬(A [])@i
6. n : ℤ@i
7. [%4] : 0 < n@i
8. tree-big(T;upwd-closure(T;A);n - 1)
⇒ (∃k:ℕn - 1. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1)))@i
9. tree-big(T;upwd-closure(T;A);n)@i
⊢ Dec(tree-big(T;upwd-closure(T;A);n - 1))

2
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. ∃k:ℕ. T ~ ℕk@i
4. Decidable(A)@i
5. ¬(A [])@i
6. n : ℤ@i
7. [%4] : 0 < n@i
8. tree-big(T;upwd-closure(T;A);n - 1)
⇒ (∃k:ℕn - 1. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1)))@i
9. tree-big(T;upwd-closure(T;A);n)@i
10. Dec(tree-big(T;upwd-closure(T;A);n - 1))
⊢ ∃k:ℕn. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1))

---

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.  \mneg{}(A  [])@i
6.  n  :  \mBbbZ{}@i
7.  [\%4]  :  0  <  n@i
8.  tree-big(T;upwd-closure(T;A);n  -  1)
{}\mRightarrow{}  (\mexists{}k:\mBbbN{}n  -  1.  ((\mneg{}tree-big(T;upwd-closure(T;A);k))  \mwedge{}  tree-big(T;upwd-closure(T;A);k  +  1)))@i
9.  tree-big(T;upwd-closure(T;A);n)@i
\mvdash{}  \mexists{}k:\mBbbN{}n.  ((\mneg{}tree-big(T;upwd-closure(T;A);k))  \mwedge{}  tree-big(T;upwd-closure(T;A);k  +  1))


By

---

Latex:
(  Assert    \mkleeneopen{}Dec(tree-big(T;upwd-closure(T;A);n  -  1))\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index