---

Step * 1 of Lemma es-first-init


1. es : EO
2. e : E
⊢ first(es-init(es;e)) = tt
BY
{ ((MoveToConcl (-1))
   THEN LocLessInd
   THEN Auto
   THEN Unfold `es-init` 0
   THEN RecUnfold `final-iterate` 0
   THEN RepUR ``can-apply do-apply`` 0
   THEN OldAutoSplit
   THEN Try (Fold `es-init` 0)
   THEN RepUR ``bfalse`` 0
   THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
\mvdash{}  first(es-init(es;e))  =  tt


By

((MoveToConcl  (-1))
  THEN  LocLessInd
  THEN  Auto
  THEN  Unfold  `es-init`  0
  THEN  RecUnfold  `final-iterate`  0
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  OldAutoSplit
  THEN  Try  (Fold  `es-init`  0)
  THEN  RepUR  ``bfalse``  0
  THEN  Auto)

---

Home Index