---

Step * of Lemma equipollent-nat-decidable-subset

No Annotations
∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) ⇒ (∀m:ℕ. ∃n:ℕ. (P[n] ∧ (m ≤ n))) ⇒ ℕ ~ {n:ℕ| P[n]} )
BY
{ (Auto
   THEN (Assert ∃d:ℕ ⟶ 𝔹. ∀n:ℕ. (↑(d n) ⇐⇒ P[n]) BY
               (RenameVar `d' (-2)
                THEN RepUR ``all decidable or`` -2
                THEN With ⌜λn.isl(d n)⌝ (D 0)⋅
                THEN Reduce 0
                THEN Auto
                THEN MoveToConcl (-1)
                THEN (GenConclTerm ⌜d n⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN Auto))
   THEN (Thin 2 THEN ExRepD)
   THEN MoveToHyp 0 (-3)
   THEN RWO  "-2<" (-1)
   THEN Auto) }

1
1. P : ℕ ⟶ ℙ
2. d : ℕ ⟶ 𝔹
3. ∀n:ℕ. (↑(d n) ⇐⇒ P[n])
4. ∀m:ℕ. ∃n:ℕ. ((↑(d n)) ∧ (m ≤ n))
⊢ ℕ ~ {n:ℕ| P[n]} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}n:\mBbbN{}.  Dec(P[n]))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (P[n]  \mwedge{}  (m  \mleq{}  n)))  {}\mRightarrow{}  \mBbbN{}  \msim{}  \{n:\mBbbN{}|  P[n]\}  )


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}d:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}n:\mBbbN{}.  (\muparrow{}(d  n)  \mLeftarrow{}{}\mRightarrow{}  P[n])  BY
                          (RenameVar  `d'  (-2)
                            THEN  RepUR  ``all  decidable  or``  -2
                            THEN  With  \mkleeneopen{}\mlambda{}n.isl(d  n)\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  MoveToConcl  (-1)
                            THEN  (GenConclTerm  \mkleeneopen{}d  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (Thin  2  THEN  ExRepD)
  THEN  MoveToHyp  0  (-3)
  THEN  RWO    "-2<"  (-1)
  THEN  Auto)

---

Home Index