---

Step * of Lemma accum-induction-lemma

∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀n:ℕ. (P[n] ⇒ P[n + 1])) ⇒ (∀n,m:ℕ.  (P[m] ⇒ P[n + m])))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN InstLemma `primrec-induction` [⌜λ2n.∀m:ℕ. (P[m] ⇒ P[n + m])⌝] ⋅ THEN Auto') }

1
1. [P] : ℕ ⟶ ℙ
2. P[0]@i
3. ∀n:ℕ. (P[n] ⇒ P[n + 1])@i
4. n : ℕ@i
5. ∀m:ℕ. (P[m] ⇒ P[n + m])@i
6. m : ℕ@i
7. P[m]@i
⊢ P[(n + 1) + m]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (P[0]  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (P[n]  {}\mRightarrow{}  P[n  +  1]))  {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}.    (P[m]  {}\mRightarrow{}  P[n  +  m])))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  InstLemma  `primrec-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mforall{}m:\mBbbN{}.  (P[m]  {}\mRightarrow{}  P[n  +  m])\mkleeneclose{}]
  \mcdot{}
  THEN  Auto')

---

Home Index