---

Step * 1 2 2 2 2 2 2 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
5. e : E@i
6. i : ℕ@i
7. i < ||[e, j]||@i
8. ¬(i = 0 ∈ ℤ)
9. ([e, j][0] <loc [e, j][i])
10. e ≤loc [e, j][0] 
11. [e, j][i] ≤loc j 
12. e ≤loc j 
13. (e <loc [e, j][i])
14. (e <loc j)
15. [e, j] = ([e, pred(j)] @ [j]) ∈ (E List)
16. ∀i:ℕ
      (i < ||[e, pred(j)]||
      ⇒ (firstn(i;[e, pred(j)]) = if (i =z 0) then [] else [e, pred([e, pred(j)][i])] fi  ∈ (E List)))
17. ¬i < ||[e, pred(j)]||
⊢ firstn(i;[e, j]) = [e, pred([e, j][i])] ∈ (E List)
BY
{ (AssertBY ⌈||[e, j]|| = (||[e, pred(j)]|| + 1) ∈ ℤ⌉
   ((HypSubst (-3) 0) THEN Auto THEN RWO "length-append" 0 THEN Auto THEN Reduce 0 THEN Auto))⋅ }

1
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 ∈ ℤ)
9. ([e, j][0] <loc [e, j][i])
10. e ≤loc [e, j][0] 
11. [e, j][i] ≤loc j 
12. e ≤loc j 
13. (e <loc [e, j][i])
14. (e <loc j)
15. [e, j] = ([e, pred(j)] @ [j]) ∈ (E List)
16. ∀i:ℕ
      (i < ||[e, pred(j)]||
      ⇒ (firstn(i;[e, pred(j)]) = if (i =z 0) then [] else [e, pred([e, pred(j)][i])] fi  ∈ (E List)))
17. ¬i < ||[e, pred(j)]||
18. ||[e, j]|| = (||[e, pred(j)]|| + 1) ∈ ℤ
⊢ 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
5.  e  :  E@i
6.  i  :  \mBbbN{}@i
7.  i  <  ||[e,  j]||@i
8.  \mneg{}(i  =  0)
9.  ([e,  j][0]  <loc  [e,  j][i])
10.  e  \mleq{}loc  [e,  j][0] 
11.  [e,  j][i]  \mleq{}loc  j 
12.  e  \mleq{}loc  j 
13.  (e  <loc  [e,  j][i])
14.  (e  <loc  j)
15.  [e,  j]  =  ([e,  pred(j)]  @  [j])
16.  \mforall{}i:\mBbbN{}
            (i  <  ||[e,  pred(j)]||
            {}\mRightarrow{}  (firstn(i;[e,  pred(j)])  =  if  (i  =\msubz{}  0)  then  []  else  [e,  pred([e,  pred(j)][i])]  fi  ))
17.  \mneg{}i  <  ||[e,  pred(j)]||
\mvdash{}  firstn(i;[e,  j])  =  [e,  pred([e,  j][i])]


By

(AssertBY  \mkleeneopen{}||[e,  j]||  =  (||[e,  pred(j)]||  +  1)\mkleeneclose{}
      ((HypSubst  (-3)  0)  THEN  Auto  THEN  RWO  "length-append"  0  THEN  Auto  THEN  Reduce  0  THEN  Auto))\mcdot{}

---

Home Index