---

Step * 1 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
{ (RW assert_pushdownC 0 THEN Auto) }

---

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{}  \muparrow{}(j  -  i  =\msubz{}  0)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(i  =\msubz{}  j)


By

---

Latex:
(RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index