---

Step * 1 1 of Lemma ses-thread-no_repeats


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)
BY
{ (D 0 THEN RepUR ``so_lambda`` 0 THEN All (Unfold `ses-thread`)⋅ THEN Auto THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES
2.  es  :  EO+(Info)
3.  thr  :  Thread
4.  \mforall{}i,j:\mBbbN{}||thr||.    (thr[i]  <loc  thr[j])  supposing  i  <  j
\mvdash{}  sorted-by(\mlambda{}\msubtwo{}a  b.(a  <loc  b);thr)


By

---

Latex:
(D  0  THEN  RepUR  ``so\_lambda``  0  THEN  All  (Unfold  `ses-thread`)\mcdot{}  THEN  Auto  THEN  Auto)

---

Home Index