---

Step * 1 1 1 1 1 1 of Lemma make-strict-agrees


1. alpha : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. strictly-increasing-seq(n;alpha)
5. i : ℕn
6. ¬make-strict(alpha) (i - 1) < alpha i
7. ¬i < 1
8. ∀i:ℕn - 1. ((make-strict(alpha) i) = (alpha i) ∈ ℤ)
⊢ ((make-strict(alpha) (i - 1)) + 1) = (alpha i) ∈ ℤ
BY
{ (D -3 THEN (RWO "-1" 0 THENA Auto)) }

1
1. alpha : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. strictly-increasing-seq(n;alpha)
5. i : ℕn
6. ¬i < 1
7. ∀i:ℕn - 1. ((make-strict(alpha) i) = (alpha i) ∈ ℤ)
⊢ alpha (i - 1) < alpha i

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  strictly-increasing-seq(n;alpha)
5.  i  :  \mBbbN{}n
6.  \mneg{}make-strict(alpha)  (i  -  1)  <  alpha  i
7.  \mneg{}i  <  1
8.  \mforall{}i:\mBbbN{}n  -  1.  ((make-strict(alpha)  i)  =  (alpha  i))
\mvdash{}  ((make-strict(alpha)  (i  -  1))  +  1)  =  (alpha  i)


By

---

Latex:
(D  -3  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index