---

Step * 1 of Lemma ses-thread-no_repeats

.....antecedent..... 
1. s : SES
2. es : EO+(Info)
3. thr : Thread
⊢ sorted-by(λ2a b.(a <loc b);thr)
BY
{ (InstLemma `ses-thread-order` [⌈s⌉;⌈es⌉;⌈thr⌉]⋅ THENA Auto) }

1
1. s : SES
2. es : EO+(Info)
3. thr : Thread
4. ∀i,j:ℕ||thr||.  (thr[i] <loc thr[j]) supposing i < j
⊢ sorted-by(λ2a b.(a <loc b);thr)

---

Latex:

---

Latex:
.....antecedent..... 
1.  s  :  SES
2.  es  :  EO+(Info)
3.  thr  :  Thread
\mvdash{}  sorted-by(\mlambda{}\msubtwo{}a  b.(a  <loc  b);thr)


By

---

Latex:
(InstLemma  `ses-thread-order`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}thr\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index