Step
*
1
2
2
1
of Lemma
from-upto-split
1. d : ℤ
2. 0 < d
3. ∀n,m:ℤ. (((m - n) ≤ (d - 1))
⇒ (∀k:ℤ. ((n ≤ k)
⇒ (k ≤ m)
⇒ ([n, m) ~ [n, k) @ [k, m)))))
4. n : ℤ
5. m : ℤ
6. ¬n < m
7. (m - n) ≤ d
8. k : ℤ
9. n ≤ k
10. k ≤ m
11. k ≤ n supposing [n, k) ~ []
12. [n, k) ~ []
⊢ [] ~ [k, m)
BY
{ ((InstLemma `from-upto-is-nil` [⌜k⌝;⌜m⌝]⋅ THENA Auto)
THEN (D (-1) THEN (D -1 THENA Auto'))
THEN HypSubst' -1 0
THEN Reduce 0)⋅ }
1
1. d : ℤ
2. 0 < d
3. ∀n,m:ℤ. (((m - n) ≤ (d - 1))
⇒ (∀k:ℤ. ((n ≤ k)
⇒ (k ≤ m)
⇒ ([n, m) ~ [n, k) @ [k, m)))))
4. n : ℤ
5. m : ℤ
6. ¬n < m
7. (m - n) ≤ d
8. k : ℤ
9. n ≤ k
10. k ≤ m
11. k ≤ n supposing [n, k) ~ []
12. [n, k) ~ []
13. m ≤ k supposing [k, m) ~ []
14. [k, m) ~ []
⊢ [] ~ []
Latex:
Latex:
1. d : \mBbbZ{}
2. 0 < d
3. \mforall{}n,m:\mBbbZ{}. (((m - n) \mleq{} (d - 1)) {}\mRightarrow{} (\mforall{}k:\mBbbZ{}. ((n \mleq{} k) {}\mRightarrow{} (k \mleq{} m) {}\mRightarrow{} ([n, m) \msim{} [n, k) @ [k, m)))))
4. n : \mBbbZ{}
5. m : \mBbbZ{}
6. \mneg{}n < m
7. (m - n) \mleq{} d
8. k : \mBbbZ{}
9. n \mleq{} k
10. k \mleq{} m
11. k \mleq{} n supposing [n, k) \msim{} []
12. [n, k) \msim{} []
\mvdash{} [] \msim{} [k, m)
By
Latex:
((InstLemma `from-upto-is-nil` [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (D (-1) THEN (D -1 THENA Auto'))
THEN HypSubst' -1 0
THEN Reduce 0)\mcdot{}
Home
Index