---

Step * 1 1 1 1 1 1 1 of Lemma es-interval-iseg


1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e2,e1:E.  (e1 ≤loc e2  ⇒ e1 ≤loc k  ⇒ ([e1, e2] ≤ [e1, k] ⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. ¬↑first(j)
9. e1 ≤loc pred(j) 
10. [e1, e2] ≤ [e1, pred(j)] ⇐⇒ e2 ≤loc pred(j) 
11. [e1, j] = ([e1, pred(j)] @ [j]) ∈ (E List)
⊢ [e1, e2] ≤ [e1, pred(j)] ∨ ([e1, e2] = ([e1, pred(j)] @ [j]) ∈ (E List)) ⇐⇒ e2 ≤loc pred(j)  ∨ (e2 = j ∈ E)
BY
{ ((RW (SweepDnC (HypC (-2))) 0) THEN Auto THEN ParallelLast) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e2,e1:E.  (e1 ≤loc e2  ⇒ e1 ≤loc k  ⇒ ([e1, e2] ≤ [e1, k] ⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. ¬↑first(j)
9. e1 ≤loc pred(j) 
10. [e1, e2] ≤ [e1, pred(j)] ⇒ e2 ≤loc pred(j) 
11. [e1, e2] ≤ [e1, pred(j)] ⇐ e2 ≤loc pred(j) 
12. [e1, j] = ([e1, pred(j)] @ [j]) ∈ (E List)
13. [e1, e2] = ([e1, pred(j)] @ [j]) ∈ (E List)@i
⊢ e2 = j ∈ E

2
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e2,e1:E.  (e1 ≤loc e2  ⇒ e1 ≤loc k  ⇒ ([e1, e2] ≤ [e1, k] ⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. ¬↑first(j)
9. e1 ≤loc pred(j) 
10. [e1, e2] ≤ [e1, pred(j)] ⇒ e2 ≤loc pred(j) 
11. [e1, e2] ≤ [e1, pred(j)] ⇐ e2 ≤loc pred(j) 
12. [e1, j] = ([e1, pred(j)] @ [j]) ∈ (E List)
13. e2 = j ∈ E@i
⊢ [e1, e2] = ([e1, pred(j)] @ [j]) ∈ (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{}e2,e1:E.    (e1  \mleq{}loc  e2    {}\mRightarrow{}  e1  \mleq{}loc  k    {}\mRightarrow{}  ([e1,  e2]  \mleq{}  [e1,  k]  \mLeftarrow{}{}\mRightarrow{}  e2  \mleq{}loc  k  ))))@i
5.  e2  :  E@i
6.  e1  :  E@i
7.  e1  \mleq{}loc  e2  @i
8.  \mneg{}\muparrow{}first(j)
9.  e1  \mleq{}loc  pred(j) 
10.  [e1,  e2]  \mleq{}  [e1,  pred(j)]  \mLeftarrow{}{}\mRightarrow{}  e2  \mleq{}loc  pred(j) 
11.  [e1,  j]  =  ([e1,  pred(j)]  @  [j])
\mvdash{}  [e1,  e2]  \mleq{}  [e1,  pred(j)]  \mvee{}  ([e1,  e2]  =  ([e1,  pred(j)]  @  [j]))  \mLeftarrow{}{}\mRightarrow{}  e2  \mleq{}loc  pred(j)    \mvee{}  (e2  =  j)


By

((RW  (SweepDnC  (HypC  (-2)))  0)  THEN  Auto  THEN  ParallelLast)

---

Home Index