---

Step * 1 2 of Lemma es-interval-select


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)))
BY
{ ((Auto THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
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
5. e : E@i
6. i : ℕ@i
7. i < ||[e, j]||@i
8. i = 0 ∈ ℤ
⊢ firstn(i;[e, j]) = [] ∈ (E List)

2
.....falsecase..... 
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
5. e : E@i
6. i : ℕ@i
7. i < ||[e, j]||@i
8. ¬(i = 0 ∈ ℤ)
⊢ firstn(i;[e, j]) = [e, pred([e, j][i])] ∈ (E List)

---

Latex:



1.  es  :  EO@i'
2.  WellFnd\{i\}(E;x,y.(x  <loc  y))
3.  j  :  E@i
4.  \mforall{}k:E
          ((k  <loc  j)
          {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}i:\mBbbN{}.
                      (i  <  ||[e,  k]||
                      {}\mRightarrow{}  (firstn(i;[e,  k])  =  if  (i  =\msubz{}  0)  then  []  else  [e,  pred([e,  k][i])]  fi  ))))@i
\mvdash{}  \mforall{}e:E.  \mforall{}i:\mBbbN{}.
        (i  <  ||[e,  j]||  {}\mRightarrow{}  (firstn(i;[e,  j])  =  if  (i  =\msubz{}  0)  then  []  else  [e,  pred([e,  j][i])]  fi  ))


By

((Auto  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index