Step * of Lemma es-interval-select

[es:EO]. ∀[e',e:E]. ∀[i:ℕ].
  firstn(i;[e, e']) if (i =z 0) then [] else [e, pred([e, e'][i])] fi  ∈ (E List) supposing i < ||[e, e']||
BY
(UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
es:EO. ∀e',e:E. ∀i:ℕ.
  (i < ||[e, e']||  (firstn(i;[e, e']) if (i =z 0) then [] else [e, pred([e, e'][i])] fi  ∈ (E List)))


Latex:


\mforall{}[es:EO].  \mforall{}[e',e:E].  \mforall{}[i:\mBbbN{}].
    firstn(i;[e,  e'])  =  if  (i  =\msubz{}  0)  then  []  else  [e,  pred([e,  e'][i])]  fi    supposing  i  <  ||[e,  e']||


By

(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))




Home Index