---

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


1. s : SES@i'
2. es : EO+(Info)@i'
3. thr : Act List@i
4. \\%2 : ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])@i
5. i : ℕ||thr||@i
6. j : ℕ||thr||@i
7. (thr[i] <loc thr[j]) supposing i < j
8. i ≤ j
9. ¬i < j
⊢ thr[i] ≤loc thr[j] 
BY
{ ((DVar `i' THEN Auto) THEN (DVar `j' THEN Auto) THEN Subst' i ~ j 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  thr  :  Act  List@i
4.  \mbackslash{}\mbackslash{}\%2  :  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])@i
5.  i  :  \mBbbN{}||thr||@i
6.  j  :  \mBbbN{}||thr||@i
7.  (thr[i]  <loc  thr[j])  supposing  i  <  j
8.  i  \mleq{}  j
9.  \mneg{}i  <  j
\mvdash{}  thr[i]  \mleq{}loc  thr[j] 


By

---

Latex:
((DVar  `i'  THEN  Auto)  THEN  (DVar  `j'  THEN  Auto)  THEN  Subst'  i  \msim{}  j  0  THEN  Auto)\mcdot{}

---

Home Index