---

Step * of Lemma decidable__exists_length_bool

∀[P:(𝔹 List) ⟶ ℙ]. ((∀L:𝔹 List. Dec(P[L])) ⇒ (∀n:ℕ. Dec(∃L:𝔹 List. ((||L|| = n ∈ ℤ) ∧ P[L]))))
BY
{ ((InstLemma `decidable__exists_length` [⌜𝔹⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN D (-1)⋅
   THEN Try (Trivial)
   THEN With ⌜2⌝ (D 0)⋅
   THEN Auto
   THEN BLemma `equipollent-two`) }

---

Latex:

---

Latex:
\mforall{}[P:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}L:\mBbbB{}  List.  Dec(P[L]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  Dec(\mexists{}L:\mBbbB{}  List.  ((||L||  =  n)  \mwedge{}  P[L]))))


By

---

Latex:
((InstLemma  `decidable\_\_exists\_length`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  D  (-1)\mcdot{}
  THEN  Try  (Trivial)
  THEN  With  \mkleeneopen{}2\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  BLemma  `equipollent-two`)

---

Home Index