---

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


1. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
2. ∀a:ℕ ⟶ ℕ. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
3. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((0s = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F 0s) = (F b) ∈ ℕ))
4. Phi : F:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ
5. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀b:ℕ ⟶ ℕ.  ((0s = b ∈ (ℕPhi F ⟶ ℕ)) ⇒ ((F 0s) = (F b) ∈ ℕ))
6. n0 : Phi* (λf.0) ~ 0s^(Phi (λf.0))
⊢ False
BY
{ ((Assert ⌜∀n0:finite-nat-seq(). ∀beta:ℕ ⟶ ℕ.
              ((∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x))))
              ∧ (∀a,b:finite-nat-seq().
                   ((↑isl(gamma-neighbourhood(beta;n0) a))
                   ⇒ ((gamma-neighbourhood(beta;n0) a) = (gamma-neighbourhood(beta;n0) a**b) ∈ (ℕ?)))))⌝⋅
    THENA ((UnivCD THENA Auto) THEN InstLemma `gamma-neighbourhood-prop1` [⌜beta⌝;⌜n1⌝]⋅ THEN Auto)
    )
   THEN (InstHyp [⌜Phi* (λf.0)⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)) }

1
1. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
2. ∀a:ℕ ⟶ ℕ. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
3. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((0s = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F 0s) = (F b) ∈ ℕ))
4. Phi : F:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ
5. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀b:ℕ ⟶ ℕ.  ((0s = b ∈ (ℕPhi F ⟶ ℕ)) ⇒ ((F 0s) = (F b) ∈ ℕ))
6. n0 : Phi* (λf.0) ~ 0s^(Phi (λf.0))
7. ∀beta:ℕ ⟶ ℕ
     ((∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) a^(x))))
     ∧ (∀a,b:finite-nat-seq().
          ((↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) a))
          ⇒ ((gamma-neighbourhood(beta;Phi* (λf.0)) a) = (gamma-neighbourhood(beta;Phi* (λf.0)) a**b) ∈ (ℕ?)))))
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  b)  {}\mRightarrow{}  ((F  a)  =  (F  b)))
2.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.    \mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  b)  {}\mRightarrow{}  ((F  a)  =  (F  b)))
3.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((0s  =  b)  {}\mRightarrow{}  ((F  0s)  =  (F  b)))
4.  Phi  :  F:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
5.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((0s  =  b)  {}\mRightarrow{}  ((F  0s)  =  (F  b)))
6.  n0  :  Phi*  (\mlambda{}f.0)  \msim{}  0s\^{}(Phi  (\mlambda{}f.0))
\mvdash{}  False


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}n0:finite-nat-seq().  \mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
                        ((\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}x:\mBbbN{}.  (\muparrow{}isl(gamma-neighbourhood(beta;n0)  a\^{}(x))))
                        \mwedge{}  (\mforall{}a,b:finite-nat-seq().
                                  ((\muparrow{}isl(gamma-neighbourhood(beta;n0)  a))
                                  {}\mRightarrow{}  ((gamma-neighbourhood(beta;n0)  a)  =  (gamma-neighbourhood(beta;n0)  a**b)))))\mkleeneclose{}\mcdot{}
    THENA  ((UnivCD  THENA  Auto)  THEN  InstLemma  `gamma-neighbourhood-prop1`  [\mkleeneopen{}beta\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{}]\mcdot{}  THEN  Auto)
    )
  THEN  (InstHyp  [\mkleeneopen{}Phi*  (\mlambda{}f.0)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2))

---

Home Index