---

Step * 1 1 2 1 1 of Lemma ses-thread-order


1. s : SES@i'
2. es : EO+(Info)@i'
3. thr : Act List@i
4. ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])@i
5. d : ℕ
6. ∀d:ℕd. ∀i,j:ℕ||thr||.  (i < j ⇒ ((j - i) ≤ d) ⇒ (thr[i] <loc thr[j]))
7. i : ℕ||thr||@i
8. j : ℕ||thr||@i
9. i < j@i
10. (j - i) ≤ d@i
11. (thr[i] <loc thr[i + 1])
12. i + 1 < j
13. (thr[i + 1] <loc thr[j])
⊢ (thr[i] <loc thr[j])
BY
{ Assert ⌈(thr[i] <loc thr[i + 1])⌉⋅ }

1
.....assertion..... 
1. s : SES@i'
2. es : EO+(Info)@i'
3. thr : Act List@i
4. ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])@i
5. d : ℕ
6. ∀d:ℕd. ∀i,j:ℕ||thr||.  (i < j ⇒ ((j - i) ≤ d) ⇒ (thr[i] <loc thr[j]))
7. i : ℕ||thr||@i
8. j : ℕ||thr||@i
9. i < j@i
10. (j - i) ≤ d@i
11. (thr[i] <loc thr[i + 1])
12. i + 1 < j
13. (thr[i + 1] <loc thr[j])
⊢ (thr[i] <loc thr[i + 1])

2
1. s : SES@i'
2. es : EO+(Info)@i'
3. thr : Act List@i
4. ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])@i
5. d : ℕ
6. ∀d:ℕd. ∀i,j:ℕ||thr||.  (i < j ⇒ ((j - i) ≤ d) ⇒ (thr[i] <loc thr[j]))
7. i : ℕ||thr||@i
8. j : ℕ||thr||@i
9. i < j@i
10. (j - i) ≤ d@i
11. (thr[i] <loc thr[i + 1])
12. i + 1 < j
13. (thr[i + 1] <loc thr[j])
14. (thr[i] <loc thr[i + 1])
⊢ (thr[i] <loc thr[j])

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  thr  :  Act  List@i
4.  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])@i
5.  d  :  \mBbbN{}
6.  \mforall{}d:\mBbbN{}d.  \mforall{}i,j:\mBbbN{}||thr||.    (i  <  j  {}\mRightarrow{}  ((j  -  i)  \mleq{}  d)  {}\mRightarrow{}  (thr[i]  <loc  thr[j]))
7.  i  :  \mBbbN{}||thr||@i
8.  j  :  \mBbbN{}||thr||@i
9.  i  <  j@i
10.  (j  -  i)  \mleq{}  d@i
11.  (thr[i]  <loc  thr[i  +  1])
12.  i  +  1  <  j
13.  (thr[i  +  1]  <loc  thr[j])
\mvdash{}  (thr[i]  <loc  thr[j])


By

---

Latex:
Assert  \mkleeneopen{}(thr[i]  <loc  thr[i  +  1])\mkleeneclose{}\mcdot{}

---

Home Index