---

Step * 1 1 1 of Lemma comp_nat_ind_tp


1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ P[i]
BY
{ (%S%
\p. let i = var_of_hyp (get_int_arg `hn` p) p in
    let z = get_distinct_var `zz' p in
    Assert
    (mk_all_term z ⌜ℕ⌝
        (mk_all_term i ⌜ℕ⌝
           (mk_uimplies
              (mk_less_than_term (mvt i) (mvt z))
              (concl p))))
    p) }

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

2
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]

---

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{}
\mvdash{}  P[i]


By

---

Latex:
(\%S\%
\mbackslash{}p.  let  i  =  var\_of\_hyp  (get\_int\_arg  `hn`  p)  p  in
        let  z  =  get\_distinct\_var  `zz'  p  in
        Assert
        (mk\_all\_term  z  \mkleeneopen{}\mBbbN{}\mkleeneclose{}
                (mk\_all\_term  i  \mkleeneopen{}\mBbbN{}\mkleeneclose{}
                      (mk\_uimplies
                            (mk\_less\_than\_term  (mvt  i)  (mvt  z))
                            (concl  p))))
        p)

---

Home Index