Step * 1 1 1 of Lemma segment_factor


1. Type
2. as List
3. {0...||as||}
4. {i...||as||}
⊢ (Π 0 ≤ i1 < i. [as[i1 i]]) (Π i ≤ k < j. [as[k]]) ∈ (T List)
BY
((RWN (LemmaWithC [`k',i] `mon_itop_shift`) THENM RW IntNormC 0) THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  as  :  T  List
3.  i  :  \{0...||as||\}
4.  j  :  \{i...||as||\}
\mvdash{}  (\mPi{}  0  \mleq{}  i1  <  j  -  i.  [as[i1  +  i]])  =  (\mPi{}  i  \mleq{}  k  <  j.  [as[k]])


By


Latex:
((RWN  1  (LemmaWithC  [`k',i]  `mon\_itop\_shift`)  0  THENM  RW  IntNormC  0)  THEN  Auto)




Home Index