---

Step * 1 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. 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))
BY
{ ((With ⌜[]⌝ (D (-1))⋅ THEN Auto)
   THEN Reduce  (-1)⋅
   THEN D -1
   THEN Auto
   THEN RepUR ``upwd-closure`` (-1)
   THEN ExRepD
   THEN FLemma `iseg_nil` [-2]
   THEN Auto
   THEN DVar `bs'
   THEN All Reduce
   THEN Auto)⋅ }

---

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.  tree-big(T;upwd-closure(T;A);0)@i
\mvdash{}  \mexists{}k:\mBbbN{}0.  ((\mneg{}tree-big(T;upwd-closure(T;A);k))  \mwedge{}  tree-big(T;upwd-closure(T;A);k  +  1))


By

---

Latex:
((With  \mkleeneopen{}[]\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)
  THEN  Reduce    (-1)\mcdot{}
  THEN  D  -1
  THEN  Auto
  THEN  RepUR  ``upwd-closure``  (-1)
  THEN  ExRepD
  THEN  FLemma  `iseg\_nil`  [-2]
  THEN  Auto
  THEN  DVar  `bs'
  THEN  All  Reduce
  THEN  Auto)\mcdot{}

---

Home Index