---

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