---

Step * 1 of Lemma basic_strong_bar_induction


1. [T] : Type
2. [R] : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. [B] : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
4. [A] : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
5. ∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])
6. ∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] ⇒ A[n;s])
7. ∀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
⊢ A[0;x]
BY
{ (RenameVar `d' (-5)
   THEN RenameVar `b' (-4)
   THEN RenameVar `i' (-3)
   THEN UseWitness ⌜bar_recursion(d;
                                  b;
                                  i;
                                  0;seq-normalize(0;x))⌝⋅
   THEN (InstLemma `bar_recursion_wf_strong` [⌜T⌝;⌜R⌝;⌜B⌝;⌜A⌝;⌜d⌝;⌜b⌝;⌜i⌝;⌜seq-normalize(0;x)⌝]⋅ THENA Auto)
   THEN DoSubsume
   THEN Try (Trivial)
   THEN GenConcl ⌜x = f ∈ (ℕ0 ⟶ T)⌝⋅
   THEN Auto
   THEN All Thin) }

1
1. T : Type
2. x : Top
⊢ x ∈ ℕ0 ⟶ T

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `d'  (-5)
  THEN  RenameVar  `b'  (-4)
  THEN  RenameVar  `i'  (-3)
  THEN  UseWitness  \mkleeneopen{}bar\_recursion(d;
                                                                b;
                                                                i;
                                                                0;seq-normalize(0;x))\mkleeneclose{}\mcdot{}
  THEN  (InstLemma  `bar\_recursion\_wf\_strong`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}seq-normalize(0;x)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  GenConcl  \mkleeneopen{}x  =  f\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  All  Thin)

---

Home Index