---

Step * of Lemma bar_recursion_wf_strong

∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[B:n:ℕ ⟶ {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))}  ⟶ ℙ].
∀[A:n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])]. ∀[b:∀n:ℕ. ∀s:R-consistent-seq(n).
                                                                                             (B[n;s] ⇒ A[n;s])].
∀[i:∀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. (bar_recursion(d;b;i;0;x) ∈ A[0;x])))
BY
{ Intros }

1
1. [T] : Type
2. [R] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. [B] : n:ℕ ⟶ {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))}  ⟶ ℙ
4. [A] : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
5. [d] : ∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])
6. [b] : ∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] ⇒ A[n;s])
7. [i] : ∀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
⊢ bar_recursion(d;
                b;
                i;
                0;x) ∈ A[0;x]

2
1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. B : n:ℕ ⟶ {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))}  ⟶ ℙ
4. A : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
5. d : ∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])
6. b : ∀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:
\mforall{}[T:Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:n:\mBbbN{}  {}\mrightarrow{}  \{s:\mBbbN{}n  {}\mrightarrow{}  T|  \mforall{}x:\mBbbN{}n.  (R  x  s  (s  x))\}    {}\mrightarrow{}  \mBbbP{}].
\mforall{}[A:n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    Dec(B[n;s])].
\mforall{}[b:\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    (B[n;s]  {}\mRightarrow{}  A[n;s])].  \mforall{}[i:\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])].
    ((\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.  (bar\_recursion(d;b;i;0;x)  \mmember{}  A[0;x])))


By

---

Latex:
Intros

---

Home Index