---

Step * 1 of Lemma nwkl!-iff-twkl!-bool

.....antecedent..... 
1. ∀A:(𝔹 List) ⟶ ℙ. (Decidable(A) ⇒ infinite-tree(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:ℕ ⟶ 𝔹. is-path(A;f)))
2. A : {A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
3. Decidable(A)
4. eff-unique-path(𝔹;A)
⊢ infinite-tree(A)
BY
{ (DVar `A' THEN Unhide) }

1
1. ∀A:(𝔹 List) ⟶ ℙ. (Decidable(A) ⇒ infinite-tree(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:ℕ ⟶ 𝔹. is-path(A;f)))
2. A : (𝔹 List) ⟶ ℙ
3. [%4] : down-closed(𝔹;A) ∧ Unbounded(A)
4. Decidable(A)
5. eff-unique-path(𝔹;A)
⊢ SqStable(infinite-tree(A))

2
1. ∀A:(𝔹 List) ⟶ ℙ. (Decidable(A) ⇒ infinite-tree(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:ℕ ⟶ 𝔹. is-path(A;f)))
2. A : (𝔹 List) ⟶ ℙ
3. down-closed(𝔹;A) ∧ Unbounded(A)
4. Decidable(A)
5. eff-unique-path(𝔹;A)
⊢ infinite-tree(A)

---

Latex:

---

Latex:
.....antecedent..... 
1.  \mforall{}A:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
          (Decidable(A)  {}\mRightarrow{}  infinite-tree(A)  {}\mRightarrow{}  eff-unique-path(\mBbbB{};A)  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  is-path(A;f)))
2.  A  :  \{A:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(\mBbbB{};A)  \mwedge{}  Unbounded(A)\} 
3.  Decidable(A)
4.  eff-unique-path(\mBbbB{};A)
\mvdash{}  infinite-tree(A)


By

---

Latex:
(DVar  `A'  THEN  Unhide)

---

Home Index