---

Step * 1 of Lemma complete-nat-induction


1. [P] : ℕ ⟶ ℙ
2. g : n:ℕ ⟶ (m:ℕn ⟶ P[m]) ⟶ P[n]@i
⊢ n:ℕ ⟶ P[n]
BY
{ (UseWitness ⌜letrec f(n)=g[n;f] in f⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  g  :  n:\mBbbN{}  {}\mrightarrow{}  (m:\mBbbN{}n  {}\mrightarrow{}  P[m])  {}\mrightarrow{}  P[n]@i
\mvdash{}  n:\mBbbN{}  {}\mrightarrow{}  P[n]


By

---

Latex:
(UseWitness  \mkleeneopen{}letrec  f(n)=g[n;f]  in  f\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index