---

Step * of Lemma basic_strong_bar_induction

No Annotations
∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[B,A:n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ].
  ((∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s]))
  ⇒ (∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] ⇒ A[n;s]))
  ⇒ (∀n:ℕ. ∀s:R-consistent-seq(n).  ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) ⇒ A[n;s]))
  ⇒ (∀alpha:{f:ℕ ⟶ T| ∀x:ℕ. (R x f (f x))} . (↓∃m:ℕ. B[m;alpha]))
  ⇒ (∀x:Top. A[0;x]))
BY
{ Intros }

1
1. [T] : Type
2. [R] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. [B] : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
4. [A] : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
5. ∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])
6. ∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] ⇒ A[n;s])
7. ∀n:ℕ. ∀s:R-consistent-seq(n).  ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) ⇒ A[n;s])
8. ∀alpha:{f:ℕ ⟶ T| ∀x:ℕ. (R x f (f x))} . (↓∃m:ℕ. B[m;alpha])
9. x : Top
⊢ A[0;x]

2
1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. B : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
4. A : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
5. ∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])
6. ∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] ⇒ A[n;s])
⊢ istype(∀n:ℕ. ∀s:R-consistent-seq(n).  ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) ⇒ A[n;s]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B,A:n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    Dec(B[n;s]))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    (B[n;s]  {}\mRightarrow{}  A[n;s]))
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    ((\mforall{}t:\{t:T|  R  n  s  t\}  .  A[n  +  1;s.t@n])  {}\mRightarrow{}  A[n;s]))
    {}\mRightarrow{}  (\mforall{}alpha:\{f:\mBbbN{}  {}\mrightarrow{}  T|  \mforall{}x:\mBbbN{}.  (R  x  f  (f  x))\}  .  (\mdownarrow{}\mexists{}m:\mBbbN{}.  B[m;alpha]))
    {}\mRightarrow{}  (\mforall{}x:Top.  A[0;x]))


By

---

Latex:
Intros

---

Home Index