---

Step * 1 of Lemma unsquashed-weak-continuity-false


1. unsquashed-WCP
⊢ ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((∀i:ℕk. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ))
BY
{ (Auto
   THEN (D 1 With ⌜F⌝  THENA Auto)
   THEN ExRepD
   THEN (D -1 With ⌜λi.0⌝  THEN Auto)
   THEN D 0 With ⌜M (λi.0)⌝ 
   THEN Auto
   THEN (BHyp 3  THEN Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  unsquashed-WCP
\mvdash{}  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}i:\mBbbN{}k.  ((g  i)  =  0))  {}\mRightarrow{}  ((F  (\mlambda{}i.0))  =  (F  g)))


By

---

Latex:
(Auto
  THEN  (D  1  With  \mkleeneopen{}F\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}i.0\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}M  (\mlambda{}i.0)\mkleeneclose{} 
  THEN  Auto
  THEN  (BHyp  3    THEN  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index