---

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


1. ∀A:(𝔹 List) ⟶ ℙ. (Decidable(A) ⇒ infinite-tree(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:ℕ ⟶ 𝔹. is-path(A;f)))
2. A : (𝔹 List) ⟶ ℙ
3. down-closed(𝔹;A)
4. Unbounded(A)
5. Decidable(A)
6. eff-unique-path(𝔹;A)
⊢ ∀n:ℕ. ∃as:𝔹 List. ((||as|| = n ∈ ℤ) ∧ (A as))
BY
{ (Fold `unbounded-list-predicate` 0 THEN Auto) }

---

Latex:

---

Latex:

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  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
3.  down-closed(\mBbbB{};A)
4.  Unbounded(A)
5.  Decidable(A)
6.  eff-unique-path(\mBbbB{};A)
\mvdash{}  \mforall{}n:\mBbbN{}.  \mexists{}as:\mBbbB{}  List.  ((||as||  =  n)  \mwedge{}  (A  as))


By

---

Latex:
(Fold  `unbounded-list-predicate`  0  THEN  Auto)

---

Home Index