---

Step * 2 of Lemma bar_recursion_wf_strong


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]))
BY
{ (UniverseIsType⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  B  :  n:\mBbbN{}  {}\mrightarrow{}  \{s:\mBbbN{}n  {}\mrightarrow{}  T|  \mforall{}x:\mBbbN{}n.  (R  x  s  (s  x))\}    {}\mrightarrow{}  \mBbbP{}
4.  A  :  n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}
5.  d  :  \mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    Dec(B[n;s])
6.  b  :  \mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    (B[n;s]  {}\mRightarrow{}  A[n;s])
\mvdash{}  istype(\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]))


By

---

Latex:
(UniverseIsType\mcdot{}  THEN  Auto)

---

Home Index