---

Step * of Lemma def-cont-induction-lemma

∀[P:ℕ ⟶ ℙ]
  ((∀n:ℕ. (P[n] ⇒ P[n + 1])) ⇒ (∀x:ℤ List. ∀[n,m:ℕ].  P[n] ⇒ P[m] supposing (x = [n, m) ∈ (ℤ List)) ∧ (n ≤ m)))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN ListInd (-1)⋅) }

1
1. [P] : ℕ ⟶ ℙ
2. ∀n:ℕ. (P[n] ⇒ P[n + 1])
⊢ ∀[n,m:ℕ].  P[n] ⇒ P[m] supposing ([] = [n, m) ∈ (ℤ List)) ∧ (n ≤ m)

2
1. [P] : ℕ ⟶ ℙ
2. ∀n:ℕ. (P[n] ⇒ P[n + 1])
3. u : ℤ
4. v : ℤ List
5. ∀[n,m:ℕ].  P[n] ⇒ P[m] supposing (v = [n, m) ∈ (ℤ List)) ∧ (n ≤ m)
⊢ ∀[n,m:ℕ].  P[n] ⇒ P[m] supposing ([u / v] = [n, m) ∈ (ℤ List)) ∧ (n ≤ m)

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}n:\mBbbN{}.  (P[n]  {}\mRightarrow{}  P[n  +  1]))
    {}\mRightarrow{}  (\mforall{}x:\mBbbZ{}  List.  \mforall{}[n,m:\mBbbN{}].    P[n]  {}\mRightarrow{}  P[m]  supposing  (x  =  [n,  m))  \mwedge{}  (n  \mleq{}  m)))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  ListInd  (-1)\mcdot{})

---

Home Index