---

Step * of Lemma nat_ind_a

∀[P:ℕ ⟶ ℙ{k}]. (P[0] ⇒ (∀i:ℕ+. (P[i - 1] ⇒ P[i])) ⇒ {∀i:ℕ. P[i]})
BY
{ ((Unfold `guard` 0 THEN Auto)
   THEN RenameVar `b' 2
   THEN (Assert ∀n:ℕ. (P[n] ⇒ P[n + 1]) BY
               (Auto THEN InstHyp [⌜n + 1⌝] 3⋅ THEN Auto' THEN NthHypSq (-1) THEN EqCD THEN Auto))
   THEN RenameVar `s' (-1)
   THEN UseWitness ⌜primrec(i;b;s)⌝⋅
   THEN Using [`P',⌜λ2i.P[i]⌝] (BLemma `primrec-wf`)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  -  1]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  \{\mforall{}i:\mBbbN{}.  P[i]\})


By

---

Latex:
((Unfold  `guard`  0  THEN  Auto)
  THEN  RenameVar  `b'  2
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (P[n]  {}\mRightarrow{}  P[n  +  1])  BY
                          (Auto  THEN  InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{}]  3\mcdot{}  THEN  Auto'  THEN  NthHypSq  (-1)  THEN  EqCD  THEN  Auto))
  THEN  RenameVar  `s'  (-1)
  THEN  UseWitness  \mkleeneopen{}primrec(i;b;s)\mkleeneclose{}\mcdot{}
  THEN  Using  [`P',\mkleeneopen{}\mlambda{}\msubtwo{}i.P[i]\mkleeneclose{}]  (BLemma  `primrec-wf`)\mcdot{}
  THEN  Auto)

---

Home Index