---

Step * 1 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])
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]
BY
{ (All (Unfold `so_apply`)⋅
   THEN (Subst' bar_recursion(d;b;i;0;x) ~ (λk,u. bar_recursion(d;b;i;k;u)) 0 x 0 THENA (Reduce 0 THEN Auto))
   THEN (Strong_Bar_Induction ⌜T⌝ ⌜R⌝ ⌜B⌝⋅ THENA Auto)⋅
   THEN (Reduce 0
         THEN Try ((Fold `decidable` 0 THEN BackThruSomeHyp))
         THEN Try (((InstHyp [⌜alpha⌝] (-4)⋅ THENA Auto) THEN Complete (RepeatFor 2 (ParallelLast))))⋅)
   THEN Reduce (-1)
   THEN RecUnfold `bar_recursion` 0⋅
   THEN All (Fold `seq-add`)
   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])
7.  [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])
8.  \mforall{}alpha:\{f:\mBbbN{}  {}\mrightarrow{}  T|  \mforall{}x:\mBbbN{}.  (R  x  f  (f  x))\}  .  (\mdownarrow{}\mexists{}m:\mBbbN{}.  B[m;alpha])
9.  x  :  Top
\mvdash{}  bar\_recursion(d;
                                b;
                                i;
                                0;x)  \mmember{}  A[0;x]


By

---

Latex:
(All  (Unfold  `so\_apply`)\mcdot{}
  THEN  (Subst'  bar\_recursion(d;b;i;0;x)  \msim{}  (\mlambda{}k,u.  bar\_recursion(d;b;i;k;u))  0  x  0  THENA  (Reduce  0  THEN\000C  Auto))
  THEN  (Strong\_Bar\_Induction  \mkleeneopen{}T\mkleeneclose{}  \mkleeneopen{}R\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (Reduce  0
              THEN  Try  ((Fold  `decidable`  0  THEN  BackThruSomeHyp))
              THEN  Try  (((InstHyp  [\mkleeneopen{}alpha\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)  THEN  Complete  (RepeatFor  2  (ParallelLast))))
              \mcdot{})
  THEN  Reduce  (-1)
  THEN  RecUnfold  `bar\_recursion`  0\mcdot{}
  THEN  All  (Fold  `seq-add`)
  THEN  Auto)

---

Home Index