Step * 2 of Lemma ni-min-nat


1. : ℕ
2. : ℕ
3. n@0 : ℕ
4. ↑(ni-min(n∞;m∞(n@0 1))
⊢ ↑(ni-min(n∞;m∞n@0)
BY
(RenameVar `i' (-2) THEN RepUR ``ni-min nat2inf`` -1 THEN RepUR ``ni-min nat2inf`` 0) }

1
1. : ℕ
2. : ℕ
3. : ℕ
4. ↑(i 1 <n ∧b 1 <m)
⊢ ↑(i <n ∧b i <m)


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n@0  :  \mBbbN{}
4.  \muparrow{}(ni-min(n\minfty{};m\minfty{})  (n@0  +  1))
\mvdash{}  \muparrow{}(ni-min(n\minfty{};m\minfty{})  n@0)


By


Latex:
(RenameVar  `i'  (-2)  THEN  RepUR  ``ni-min  nat2inf``  -1  THEN  RepUR  ``ni-min  nat2inf``  0)




Home Index