---

Step * of Lemma bar_recursion_wf0

∀[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])) ⇒ (bar_recursion(d;b;i;0;λm.eval x = m in ⊥) ∈ A[0;λm.⊥]))
BY
{ (InstLemma `bar_recursion_wf1` [] THEN RepeatFor 7 ((ParallelLast' THENA 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])
⊢ bar_recursion(d;
                b;
                i;
                0;λm.eval x = m in
                     ⊥) ∈ A[0;λm.⊥]

---

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{}  (bar\_recursion(d;b;i;0;\mlambda{}m.eval  x  =  m  in  \mbot{})  \mmember{}  A[0;\mlambda{}m.\mbot{}]))


By

---

Latex:
(InstLemma  `bar\_recursion\_wf1`  []  THEN  RepeatFor  7  ((ParallelLast'  THENA  Auto)))

---

Home Index