---

Step * 1 1 1 2 of Lemma comp_nat_ind_tp


1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
4. ∀zz,i:ℕ.  P[i] supposing i < zz
⊢ P[i]
BY
{ (\p.let i = mvt (var_of_hyp (-2) p) in
   let ip1 = mk_add_term  i ⌜1⌝ in
   (DTerm ip1 (-1) THENM DTerm i (-1)) p) }

1
.....wf..... 
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ i + 1 ∈ ℕ

2
.....wf..... 
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ i ∈ ℕ

3
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
4. P[i] supposing i < i + 1
⊢ P[i]

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i])
3.  i  :  \mBbbN{}
4.  \mforall{}zz,i:\mBbbN{}.    P[i]  supposing  i  <  zz
\mvdash{}  P[i]


By

---

Latex:
(\mbackslash{}p.let  i  =  mvt  (var\_of\_hyp  (-2)  p)  in
      let  ip1  =  mk\_add\_term    i  \mkleeneopen{}1\mkleeneclose{}  in
      (DTerm  ip1  (-1)  THENM  DTerm  i  (-1))  p)

---

Home Index