---

Step * of Lemma complete_nat_ind_with_y

∀[P:ℕ ⟶ ℙ{k}]. ((∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
BY
{ ((InstLemma `complete_nat_measure_ind` [⌜parm{k}⌝;⌜ℕ⌝;⌜λ2n.n⌝]⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast)
   THEN Auto
   THEN BHyp -2 ) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}].  ((\mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}i.  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))


By

---

Latex:
((InstLemma  `complete\_nat\_measure\_ind`  [\mkleeneopen{}parm\{k\}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast)
  THEN  Auto
  THEN  BHyp  -2  )

---

Home Index