---

Step * 1 2 1 1 1 2 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. ∀as:T List. (¬((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as))))
7. as : T List@i
8. ¬((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as)))
9. ||as|| = n ∈ ℤ@i
10. Dec(upwd-closure(T;A) as)
⊢ upwd-closure(T;A) as
BY
{ (D (-1) THEN Auto) }

1
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. ∃k:ℕ. T ~ ℕk@i
4. Decidable(A)@i
5. n : ℕ@i
6. ∀as:T List. (¬((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as))))
7. as : T List@i
8. ¬((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as)))
9. ||as|| = n ∈ ℤ@i
10. ¬(upwd-closure(T;A) as)
⊢ 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.  \mforall{}as:T  List.  (\mneg{}((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;A)  as))))
7.  as  :  T  List@i
8.  \mneg{}((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;A)  as)))
9.  ||as||  =  n@i
10.  Dec(upwd-closure(T;A)  as)
\mvdash{}  upwd-closure(T;A)  as


By

---

Latex:
(D  (-1)  THEN  Auto)

---

Home Index