---

Step * 1 of Lemma es-init-le


1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ¬↑first(j)
5. ∀k:E. ((k <loc j) ⇒ (es-init(es;k) ≤loc k  ⇐⇒ True))@i
6. True@i
⊢ es-init(es;pred(j)) ≤loc j 
BY
{ ((InstLemma `es-pred-locl` [⌈es⌉;⌈j⌉]⋅ THENA Auto)
   THEN ((Assert es-init(es;pred(j)) ≤loc pred(j)  BY (BackThruSomeHyp THEN Auto)) THEN Auto)
   ) }

---

Latex:



1.  es  :  EO@i'
2.  WellFnd\{i\}(E;x,y.(x  <loc  y))
3.  j  :  E@i
4.  \mneg{}\muparrow{}first(j)
5.  \mforall{}k:E.  ((k  <loc  j)  {}\mRightarrow{}  (es-init(es;k)  \mleq{}loc  k    \mLeftarrow{}{}\mRightarrow{}  True))@i
6.  True@i
\mvdash{}  es-init(es;pred(j))  \mleq{}loc  j 


By

((InstLemma  `es-pred-locl`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((Assert  es-init(es;pred(j))  \mleq{}loc  pred(j)    BY  (BackThruSomeHyp  THEN  Auto))  THEN  Auto)
  )

---

Home Index