Step
*
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
⊢ (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
⊢ (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])
⊢ (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
\mvdash{} (thr[i] <loc thr[j])
By
Latex:
Assert \mkleeneopen{}(thr[i] <loc thr[i + 1])\mkleeneclose{}\mcdot{}
Home
Index