Step
*
1
1
1
1
of Lemma
unsquashed-BIM-implies-unsquashed-weak-continuity
1. ∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n])
⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ. (B[n;s]
⇒ B[n + 1;s.m@n]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s]
⇒ Q[n;s]))
⇒ Q[0;λx.⊥])
2. F : (ℕ ⟶ ℕ) ⟶ ℕ
3. a : ℕ ⟶ ℕ
4. n : ℕ
5. s : ℕn ⟶ ℕ
6. ∀m:ℕ
∃n@0:{n + 1...}
∀b:ℕ ⟶ ℕ
((∀i:ℕn@0. ((rep-seq-from(s.m@n;n + 1;a) i) = (b i) ∈ ℕ))
⇒ ((F rep-seq-from(s.m@n;n + 1;a)) = (F b) ∈ ℕ))
7. k : {n + 1...}
8. ∀b:ℕ ⟶ ℕ
((∀i:ℕk. ((rep-seq-from(s.a n@n;n + 1;a) i) = (b i) ∈ ℕ))
⇒ ((F rep-seq-from(s.a n@n;n + 1;a)) = (F b) ∈ ℕ))
9. b : ℕ ⟶ ℕ
10. ∀i:ℕk. ((rep-seq-from(s;n;a) i) = (b i) ∈ ℕ)
11. i : ℕk
⊢ (rep-seq-from(s.a n@n;n + 1;a) i) = (b i) ∈ ℕ
BY
{ ((InstLemma `rep-seq-from-prop3` [⌜ℕ⌝;⌜n⌝;⌜s⌝;⌜a⌝]⋅ THENA Auto) THEN HypSubst' (-1) (-2) THEN Auto) }
Latex:
Latex:
1. \mforall{}B,Q:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}.
((\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. ((\mforall{}m:\mBbbN{}. Q[n + 1;s.m@n]) {}\mRightarrow{} Q[n;s]))
{}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. B[n;f]))
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. \mforall{}m:\mBbbN{}. (B[n;s] {}\mRightarrow{} B[n + 1;s.m@n]))
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. (B[n;s] {}\mRightarrow{} Q[n;s]))
{}\mRightarrow{} Q[0;\mlambda{}x.\mbot{}])
2. F : (\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}
3. a : \mBbbN{} {}\mrightarrow{} \mBbbN{}
4. n : \mBbbN{}
5. s : \mBbbN{}n {}\mrightarrow{} \mBbbN{}
6. \mforall{}m:\mBbbN{}
\mexists{}n@0:\{n + 1...\}
\mforall{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{}
((\mforall{}i:\mBbbN{}n@0. ((rep-seq-from(s.m@n;n + 1;a) i) = (b i)))
{}\mRightarrow{} ((F rep-seq-from(s.m@n;n + 1;a)) = (F b)))
7. k : \{n + 1...\}
8. \mforall{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{}
((\mforall{}i:\mBbbN{}k. ((rep-seq-from(s.a n@n;n + 1;a) i) = (b i)))
{}\mRightarrow{} ((F rep-seq-from(s.a n@n;n + 1;a)) = (F b)))
9. b : \mBbbN{} {}\mrightarrow{} \mBbbN{}
10. \mforall{}i:\mBbbN{}k. ((rep-seq-from(s;n;a) i) = (b i))
11. i : \mBbbN{}k
\mvdash{} (rep-seq-from(s.a n@n;n + 1;a) i) = (b i)
By
Latex:
((InstLemma `rep-seq-from-prop3` [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{} THENA Auto) THEN HypSubst' (-1) (-2) THEN Auto)
Home
Index