---

Step * 1 1 of Lemma es-interface-predecessors-sorted-by-le


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. ∀i:ℕ||≤(X)(e)||. ∀j:ℕi.  (≤(X)(e)[j] <loc ≤(X)(e)[i])
⊢ ∀i:ℕ||≤(X)(e)||. ∀j:ℕi.  ≤(X)(e)[j] ≤loc ≤(X)(e)[i] 
BY
{ (Auto THEN InstHyp [⌈i⌉;⌈j⌉] (-3)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  e  :  E@i
5.  \mforall{}i:\mBbbN{}||\mleq{}(X)(e)||.  \mforall{}j:\mBbbN{}i.    (\mleq{}(X)(e)[j]  <loc  \mleq{}(X)(e)[i])
\mvdash{}  \mforall{}i:\mBbbN{}||\mleq{}(X)(e)||.  \mforall{}j:\mBbbN{}i.    \mleq{}(X)(e)[j]  \mleq{}loc  \mleq{}(X)(e)[i] 


By

---

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

---

Home Index