---

Step * of Lemma bar_recursion_wf1

∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(R[n;s])].
∀[b:∀n:ℕ. ∀s:ℕn ⟶ T.  (R[n;s] ⇒ A[n;s])]. ∀[i:∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])].
  ((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[m;alpha])) ⇒ (∀c:Top. (bar_recursion(d;b;i;0;c) ∈ A[0;c])))
BY
{ Auto }

1
1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
4. d : ∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(R[n;s])
5. b : ∀n:ℕ. ∀s:ℕn ⟶ T.  (R[n;s] ⇒ A[n;s])
6. i : ∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])
7. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[m;alpha])
8. c : Top
⊢ bar_recursion(d;
                b;
                i;
                0;c) ∈ A[0;c]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    Dec(R[n;s])].  \mforall{}[b:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
                                                                                                                                                                        (R[n;s]
                                                                                                                                                                        {}\mRightarrow{}  A[n;s])].
\mforall{}[i:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    ((\mforall{}t:T.  A[n  +  1;seq-append(n;1;s;\mlambda{}i.t)])  {}\mRightarrow{}  A[n;s])].
    ((\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}m:\mBbbN{}.  R[m;alpha]))  {}\mRightarrow{}  (\mforall{}c:Top.  (bar\_recursion(d;b;i;0;c)  \mmember{}  A[0;c])))


By

---

Latex:
Auto

---

Home Index