Step
*
1
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 : ℕ ⟶ ℕ
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 ∈ ℕ
BY
{ (MoveToConcl (-3)
THEN RepUR ``gamma-neighbourhood`` 0
THEN (BoolCase ⌜init-seg-nat-seq(x^(x@0);Phi* (λf.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. (Psi beta x) = outl(gamma-neighbourhood(beta;Phi* (λf.0)) x^(x@0)) ∈ ℕ
15. ∀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) ∈ (ℕ?)))
16. ↑init-seg-nat-seq(x^(x@0);Phi* (λf.0))
⊢ False ⇒ (⊥ = 0 ∈ ℕ)
2
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. ¬↑init-seg-nat-seq(x^(x@0);Phi* (λf.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) ∈ (ℕ?)))
⊢ (↑isl(if TERMOF{extend-seq1-all-dec:o, 1:l} x^(x@0) (Phi* (λf.0)) beta then inl 1 else inl 0 fi ))
⇒ (outl(if TERMOF{extend-seq1-all-dec:o, 1:l} x^(x@0) (Phi* (λf.0)) beta then inl 1 else inl 0 fi ) = 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{}
13. x@0 : \mBbbN{}
14. \muparrow{}isl(gamma-neighbourhood(beta;Phi* (\mlambda{}f.0)) x\^{}(x@0))
15. (Psi beta x) = outl(gamma-neighbourhood(beta;Phi* (\mlambda{}f.0)) x\^{}(x@0))
16. \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)))
\mvdash{} outl(gamma-neighbourhood(beta;Phi* (\mlambda{}f.0)) x\^{}(x@0)) = 0
By
Latex:
(MoveToConcl (-3)
THEN RepUR ``gamma-neighbourhood`` 0
THEN (BoolCase \mkleeneopen{}init-seg-nat-seq(x\^{}(x@0);Phi* (\mlambda{}f.0))\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index