Step
*
1
3
of Lemma
monotone-bar-induction8-2
1. Q : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
2. ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n])
⇒ Q[n;s])
3. bar : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f])
4. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
5. ∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
(((λf,n. ∀m:{n...}. Q[m;f]) f k)
∧ ((M n f) = (inl k) ∈ (ℕ?))
∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?)))))
6. alpha : ℕ ⟶ ℕ
⊢ ↓∃m:ℕ. (↑isl(M m alpha))
BY
{ ((InstHyp [⌜alpha⌝] (-2)⋅ THENA Auto) THEN ExRepD THEN D 0 THEN With ⌜n⌝ (D 0)⋅ THEN Auto) }
Latex:
Latex:
1. Q : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}
2. \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. ((\mforall{}m:\mBbbN{}. Q[n + 1;s.m@n]) {}\mRightarrow{} Q[n;s])
3. bar : \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. Q[m;f])
4. M : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} (\mBbbN{}n?)
5. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
\mexists{}n:\mBbbN{}
\mexists{}k:\mBbbN{}n
(((\mlambda{}f,n. \mforall{}m:\{n...\}. Q[m;f]) f k)
\mwedge{} ((M n f) = (inl k))
\mwedge{} (\mforall{}m:\mBbbN{}. ((\muparrow{}isl(M m f)) {}\mRightarrow{} ((M m f) = (inl k)))))
6. alpha : \mBbbN{} {}\mrightarrow{} \mBbbN{}
\mvdash{} \mdownarrow{}\mexists{}m:\mBbbN{}. (\muparrow{}isl(M m alpha))
By
Latex:
((InstHyp [\mkleeneopen{}alpha\mkleeneclose{}] (-2)\mcdot{} THENA Auto) THEN ExRepD THEN D 0 THEN With \mkleeneopen{}n\mkleeneclose{} (D 0)\mcdot{} THEN Auto)
Home
Index