---

Step * 1 1 of Lemma strong-continuity2-implies-weak-skolem2


1. G : (ℕ ⟶ ℕ2) ⟶ ℕ
⊢ ⇃(weak-continuity-skolem(ℕ2;G))
BY
{ ((Assert ⇃(basic-strong-continuity(ℕ2;G)) BY
          (UseWitness ⌜Kleene-M(G)⌝⋅
           THEN Auto
           THEN MemTypeCD
           THEN Auto
           THEN D 0
           THEN Auto
           THEN UseWitness ⌜0⌝⋅
           THEN Auto))
   THEN MoveToConcl (-1)
   THEN BLemma `implies-quotient-true`
   THEN Auto) }

1
1. G : (ℕ ⟶ ℕ2) ⟶ ℕ
2. basic-strong-continuity(ℕ2;G)
⊢ weak-continuity-skolem(ℕ2;G)

---

Latex:

---

Latex:

1.  G  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{}2)  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \00D9(weak-continuity-skolem(\mBbbN{}2;G))


By

---

Latex:
((Assert  \00D9(basic-strong-continuity(\mBbbN{}2;G))  BY
                (UseWitness  \mkleeneopen{}Kleene-M(G)\mkleeneclose{}\mcdot{}
                  THEN  Auto
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  D  0
                  THEN  Auto
                  THEN  UseWitness  \mkleeneopen{}0\mkleeneclose{}\mcdot{}
                  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `implies-quotient-true`
  THEN  Auto)

---

Home Index