---

Step * 1 of Lemma rec-nat-induction


1. [P] : ℕ ⟶ ℙ
2. Top ⊆r P[0]
3. f : ∀[n:ℕ]. (P[n] ⇒ P[n + 1])@i
⊢ ∀[n:ℕ]. P[n]
BY
{ (All (Unfold `uall`)⋅
   THEN UseWitness ⌜fix(f)⌝⋅
   THEN Try (Complete (Auto))
   THEN (MemTypeCD THENA Auto)
   THEN primNatInd (-1)) }

1
.....basecase..... 
1. P : ℕ ⟶ ℙ
2. Top ⊆r P[0]
3. f : ⋂n:ℕ. (P[n] ⇒ P[n + 1])@i
4. n : ℤ
⊢ fix(f) ∈ P[0]

2
.....upcase..... 
1. P : ℕ ⟶ ℙ
2. Top ⊆r P[0]
3. f : ⋂n:ℕ. (P[n] ⇒ P[n + 1])@i
4. n : ℤ
5. 0 < n
6. fix(f) ∈ P[n - 1]
⊢ fix(f) ∈ P[n]

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  Top  \msubseteq{}r  P[0]
3.  f  :  \mforall{}[n:\mBbbN{}].  (P[n]  {}\mRightarrow{}  P[n  +  1])@i
\mvdash{}  \mforall{}[n:\mBbbN{}].  P[n]


By

---

Latex:
(All  (Unfold  `uall`)\mcdot{}
  THEN  UseWitness  \mkleeneopen{}fix(f)\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  (MemTypeCD  THENA  Auto)
  THEN  primNatInd  (-1))

---

Home Index