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 (ParallelLast)
   THEN (-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