---

Step * of Lemma null-segment

∀[T:Type]. ∀[as:T List]. ∀[i:{0...||as||}]. ∀[j:{i...||as||}].  null(as[i..j-]) = (i =z j)
BY
{ (InstLemma `length_segment` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (RWO  "null-length-zero" 0 THENA Auto)
   THEN (RWO "length_segment" 0 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:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[i:\{0...||as||\}].  \mforall{}[j:\{i...||as||\}].    null(as[i..j\msupminus{}])  =  (i  =\msubz{}  j)


By

---

Latex:
(InstLemma  `length\_segment`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (RWO    "null-length-zero"  0  THENA  Auto)
  THEN  (RWO  "length\_segment"  0  THENA  Auto))

---

Home Index