---

Step * 1 of Lemma es-interval-select


∀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)))
BY
{ (((D 0 THENA Auto) THEN LocLessInd)
   THENA (Try (Complete (Auto)) THEN RepeatFor 5 ((MemCD THEN Try (Complete (Auto)))) THEN SplitOnConclITE THEN Auto)
   ) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. e' : E@i
4. e : E@i
5. i : ℕ@i
6. i < ||[e, e']||
7. ¬(i = 0 ∈ ℤ)
⊢ ¬↑first([e, e'][i])

2
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E
     ((k <loc j)
     ⇒ (∀e:E. ∀i:ℕ.
           (i < ||[e, k]|| ⇒ (firstn(i;[e, k]) = if (i =z 0) then [] else [e, pred([e, k][i])] fi  ∈ (E List)))))@i
⊢ ∀e:E. ∀i:ℕ.  (i < ||[e, j]|| ⇒ (firstn(i;[e, j]) = if (i =z 0) then [] else [e, pred([e, j][i])] fi  ∈ (E List)))

3
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. k : E@i
5. (k <loc j)
6. e : E@i
7. i : ℕ@i
8. i < ||[e, k]||
9. ¬(i = 0 ∈ ℤ)
⊢ ¬↑first([e, k][i])

---

Latex:



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


By

(((D  0  THENA  Auto)  THEN  LocLessInd)
  THENA  (Try  (Complete  (Auto))
                THEN  RepeatFor  5  ((MemCD  THEN  Try  (Complete  (Auto))))
                THEN  SplitOnConclITE
                THEN  Auto)
  )

---

Home Index