---

Step * of Lemma es-init-le

∀es:EO. ∀e:E.  (es-init(es;e) ≤loc e  ⇐⇒ True)
BY
{ ((LocLessInd THENA Auto)
   THEN Unfold `es-init` 0
   THEN RecUnfold `final-iterate` 0
   THEN RepUR ``can-apply do-apply`` 0
   THEN (BoolCase ⌈first(j)⌉⋅ THENA Auto)
   THEN Try (Fold `es-init` 0)
   THEN RepUR ``bfalse`` 0
   THEN Auto) }

1
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 

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.    (es-init(es;e)  \mleq{}loc  e    \mLeftarrow{}{}\mRightarrow{}  True)


By

((LocLessInd  THENA  Auto)
  THEN  Unfold  `es-init`  0
  THEN  RecUnfold  `final-iterate`  0
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  (BoolCase  \mkleeneopen{}first(j)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Fold  `es-init`  0)
  THEN  RepUR  ``bfalse``  0
  THEN  Auto)

---

Home Index