---

Step * 2 of Lemma ses-thread-order


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
BY
{ ((D 3 THEN Auto) THEN InstHyp [⌈j - i⌉;⌈i⌉;⌈j⌉] (-4)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  thr  :  Thread@i
4.  \mforall{}d:\mBbbN{}.  \mforall{}i,j:\mBbbN{}||thr||.    (i  <  j  {}\mRightarrow{}  ((j  -  i)  \mleq{}  d)  {}\mRightarrow{}  (thr[i]  <loc  thr[j]))
\mvdash{}  \mforall{}i,j:\mBbbN{}||thr||.    (thr[i]  <loc  thr[j])  supposing  i  <  j


By

---

Latex:
((D  3  THEN  Auto)  THEN  InstHyp  [\mkleeneopen{}j  -  i\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto')

---

Home Index