---

Step * 1 1 1 1 1 1 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))
7. ∀beta,a:ℕ ⟶ ℕ.
     ∃y,x:ℕ
      ((↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) a^(x)))
      ∧ (y = outl(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) ∈ (ℕ?)))))
8. Psi : beta:(ℕ ⟶ ℕ) ⟶ a:(ℕ ⟶ ℕ) ⟶ ℕ
9. ∀beta,a:ℕ ⟶ ℕ.
     ∃x:ℕ
      ((↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) a^(x)))
      ∧ ((Psi beta a) = outl(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) ∈ (ℕ?)))))
10. beta : ℕ ⟶ ℕ
11. ∀x:ℕ. ((beta x) = 0 ∈ ℤ)
12. x : ℕ ⟶ ℕ
⊢ (Psi beta x) = 0 ∈ ℕ
BY
{ ((InstHyp [⌜beta⌝;⌜x⌝] (-4)⋅ THENA Auto) THEN ExRepD THEN (HypSubst' (-2) 0 THENA Auto)) }

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:ℕ ⟶ ℕ.
     ∃y,x:ℕ
      ((↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) a^(x)))
      ∧ (y = outl(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) ∈ (ℕ?)))))
8. Psi : beta:(ℕ ⟶ ℕ) ⟶ a:(ℕ ⟶ ℕ) ⟶ ℕ
9. ∀beta,a:ℕ ⟶ ℕ.
     ∃x:ℕ
      ((↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) a^(x)))
      ∧ ((Psi beta a) = outl(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) ∈ (ℕ?)))))
10. beta : ℕ ⟶ ℕ
11. ∀x:ℕ. ((beta x) = 0 ∈ ℤ)
12. x : ℕ ⟶ ℕ
13. x@0 : ℕ
14. ↑isl(gamma-neighbourhood(beta;Phi* (λf.0)) x^(x@0))
15. (Psi beta x) = outl(gamma-neighbourhood(beta;Phi* (λf.0)) x^(x@0)) ∈ ℕ
16. ∀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) ∈ (ℕ?)))
⊢ outl(gamma-neighbourhood(beta;Phi* (λf.0)) x^(x@0)) = 0 ∈ ℕ

---

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))
7.  \mforall{}beta,a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
          \mexists{}y,x:\mBbbN{}
            ((\muparrow{}isl(gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a\^{}(x)))
            \mwedge{}  (y  =  outl(gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a\^{}(x)))
            \mwedge{}  (\mforall{}a,b:finite-nat-seq().
                      ((\muparrow{}isl(gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a))
                      {}\mRightarrow{}  ((gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a)
                            =  (gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a**b)))))
8.  Psi  :  beta:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  a:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
9.  \mforall{}beta,a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.
          \mexists{}x:\mBbbN{}
            ((\muparrow{}isl(gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a\^{}(x)))
            \mwedge{}  ((Psi  beta  a)  =  outl(gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a\^{}(x)))
            \mwedge{}  (\mforall{}a,b:finite-nat-seq().
                      ((\muparrow{}isl(gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a))
                      {}\mRightarrow{}  ((gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a)
                            =  (gamma-neighbourhood(beta;Phi*  (\mlambda{}f.0))  a**b)))))
10.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
11.  \mforall{}x:\mBbbN{}.  ((beta  x)  =  0)
12.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  (Psi  beta  x)  =  0


By

---

Latex:
((InstHyp  [\mkleeneopen{}beta\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  (HypSubst'  (-2)  0  THENA  Auto))

---

Home Index