---

Step * 1 of Lemma null-segment


1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
5. ||as[i..j-]|| = (j - i) ∈ ℤ
⊢ (j - i =z 0) = (i =z j)
BY
{ (BLemma `iff_imp_equal_bool` THENA Auto) }

1
1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
5. ||as[i..j-]|| = (j - i) ∈ ℤ
⊢ ↑(j - i =z 0) ⇐⇒ ↑(i =z j)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  i  :  \{0...||as||\}
4.  j  :  \{i...||as||\}
5.  ||as[i..j\msupminus{}]||  =  (j  -  i)
\mvdash{}  (j  -  i  =\msubz{}  0)  =  (i  =\msubz{}  j)


By

---

Latex:
(BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)

---

Home Index