---

Step * of Lemma ses-thread-order

∀s:SES. ∀es:EO+(Info). ∀thr:Thread. ∀i,j:ℕ||thr||.  (thr[i] <loc thr[j]) supposing i < j
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN Assert ⌜∀d:ℕ. ∀i,j:ℕ||thr||.  (i < j ⇒ ((j - i) ≤ d) ⇒ (thr[i] <loc thr[j]))⌝⋅
   ) }

1
.....assertion..... 
1. s : SES@i'
2. es : EO+(Info)@i'
3. thr : Thread@i
⊢ ∀d:ℕ. ∀i,j:ℕ||thr||.  (i < j ⇒ ((j - i) ≤ d) ⇒ (thr[i] <loc thr[j]))

2
1. s : SES@i'
2. es : EO+(Info)@i'
3. thr : Thread@i
4. ∀d:ℕ. ∀i,j:ℕ||thr||.  (i < j ⇒ ((j - i) ≤ d) ⇒ (thr[i] <loc thr[j]))
⊢ ∀i,j:ℕ||thr||.  (thr[i] <loc thr[j]) supposing i < j

---

Latex:

---

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).  \mforall{}thr:Thread.  \mforall{}i,j:\mBbbN{}||thr||.    (thr[i]  <loc  thr[j])  supposing  i  <  j


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}i,j:\mBbbN{}||thr||.    (i  <  j  {}\mRightarrow{}  ((j  -  i)  \mleq{}  d)  {}\mRightarrow{}  (thr[i]  <loc  thr[j]))\mkleeneclose{}\mcdot{}
  )

---

Home Index