---

Step * 1 of Lemma es-interface-predecessors-cases


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
⊢ ≤(X)(e) ~ if e ∈b X then if first(e) then [e] else ≤(X)(pred(e)) @ [e] fi 
if first(e) then []
else ≤(X)(pred(e))
fi 
BY
{ (RepUR ``es-interface-predecessors es-le-before eclass-events`` 0
   THEN RW (AddrC [1] (RecUnfoldC `es-before`)) 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0
   THEN Try (Trivial)) }

1
.....falsecase..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ¬↑first(e)
⊢ filter(λe.e ∈b X;(before(pred(e)) @ [pred(e)]) @ [e]) ~ if e ∈b X
then filter(λe.e ∈b X;before(pred(e)) @ [pred(e)]) @ [e]
else filter(λe.e ∈b X;before(pred(e)) @ [pred(e)])
fi 

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  e  :  E
\mvdash{}  \mleq{}(X)(e)  \msim{}  if  e  \mmember{}\msubb{}  X  then  if  first(e)  then  [e]  else  \mleq{}(X)(pred(e))  @  [e]  fi 
if  first(e)  then  []
else  \mleq{}(X)(pred(e))
fi 


By

---

Latex:
(RepUR  ``es-interface-predecessors  es-le-before  eclass-events``  0
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `es-before`))  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index