---

Step * 1 1 of Lemma es-interval-last


1. es : EO
2. e2 : E
3. e1 : E
4. e1 ≤loc e2 
⊢ last(filter(λev.e1 ≤loc ev;before(e2)) @ filter(λev.e1 ≤loc ev;[e2])) ~ e2
BY
{ (((RWO "last_append" 0
     THEN Try (Complete (Auto))
     THEN Try ((DoSubsume THEN Auto THEN UseSubtypeRelLemmas THEN Auto THEN D 0 THEN Auto))
     THEN Reduce 0
     THEN SplitOnConclITE
     THEN Reduce 0)
    THENA Auto
    )
   THEN Try (Complete (Auto))
   ) }

---

Latex:



1.  es  :  EO
2.  e2  :  E
3.  e1  :  E
4.  e1  \mleq{}loc  e2 
\mvdash{}  last(filter(\mlambda{}ev.e1  \mleq{}loc  ev;before(e2))  @  filter(\mlambda{}ev.e1  \mleq{}loc  ev;[e2]))  \msim{}  e2


By

(((RWO  "last\_append"  0
      THEN  Try  (Complete  (Auto))
      THEN  Try  ((DoSubsume  THEN  Auto  THEN  UseSubtypeRelLemmas  THEN  Auto  THEN  D  0  THEN  Auto))
      THEN  Reduce  0
      THEN  SplitOnConclITE
      THEN  Reduce  0)
    THENA  Auto
    )
  THEN  Try  (Complete  (Auto))
  )

---

Home Index