Step
*
1
of Lemma
from-upto-member-nat
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. (k ∈ [n, m))
⊢ (n ≤ k) ∧ k < m
BY
{ (RepeatFor 2 (D (-1)) THEN (RWO "length-from-upto" (-2) THENA Auto) THEN (SplitOnHypITE -2 THENA Auto)) }
1
.....truecase.....
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. i : ℕ
5. i < m - n
6. k = [n, m)[i] ∈ ℕ
7. n < m
⊢ (n ≤ k) ∧ k < m
2
.....falsecase.....
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. i : ℕ
5. i < 0
6. k = [n, m)[i] ∈ ℕ
7. ¬n < m
⊢ (n ≤ k) ∧ k < m
Latex:
Latex:
1. n : \mBbbN{}
2. m : \mBbbN{}
3. k : \mBbbN{}
4. (k \mmember{} [n, m))
\mvdash{} (n \mleq{} k) \mwedge{} k < m
By
Latex:
(RepeatFor 2 (D (-1))
THEN (RWO "length-from-upto" (-2) THENA Auto)
THEN (SplitOnHypITE -2 THENA Auto))
Home
Index