---

Step * of Lemma tree-big-least

∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
  ((∃k:ℕ. T ~ ℕk)
  ⇒ Decidable(A)
  ⇒ (¬(A []))
  ⇒ (∀n:ℕ
        (tree-big(T;upwd-closure(T;A);n)
        ⇒ (∃k:ℕn. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1))))))
BY
{ (InductionOnNat THEN Auto) }

1
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. ∃k:ℕ. T ~ ℕk@i
4. Decidable(A)@i
5. ¬(A [])@i
6. tree-big(T;upwd-closure(T;A);0)@i
⊢ ∃k:ℕ0. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 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
⊢ ∃k:ℕn. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)
    {}\mRightarrow{}  Decidable(A)
    {}\mRightarrow{}  (\mneg{}(A  []))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}
                (tree-big(T;upwd-closure(T;A);n)
                {}\mRightarrow{}  (\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:
(InductionOnNat  THEN  Auto)

---

Home Index