---

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

.....wf..... 
1. ∀A:{A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
     (Decidable(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:{ℕ ⟶ 𝔹| is-path(A;f)}))
2. A : (𝔹 List) ⟶ ℙ
3. Decidable(A)
4. infinite-tree(A)
5. eff-unique-path(𝔹;A)
⊢ A ∈ {A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
BY
{ (D (-2) THEN MemTypeCD THEN Auto) }

1
1. ∀A:{A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
     (Decidable(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:{ℕ ⟶ 𝔹| is-path(A;f)}))
2. A : (𝔹 List) ⟶ ℙ
3. Decidable(A)
4. ∀as,bs:𝔹 List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
5. ∀n:ℕ. ∃as:𝔹 List. ((||as|| = n ∈ ℤ) ∧ (A as))
6. eff-unique-path(𝔹;A)
⊢ down-closed(𝔹;A)

---

Latex:

---

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


By

---

Latex:
(D  (-2)  THEN  MemTypeCD  THEN  Auto)

---

Home Index