---

Step * 2 of Lemma es-interface-predecessors-general-step


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
⊢ ≤(X)(e) = (if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  @ if e ∈b X then [e] else [] fi ) ∈ (E(X) List)
BY
{ (RW (AddrC [2] (UnfoldC `es-interface-predecessors`)) 0
   THEN Unfold `eclass-events` 0
   THEN Unfold `es-le-before` 0
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN Reduce 0
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
1:n
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
⊢ filter(λe.e ∈b X;before(e)) = if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  ∈ (E(X) List)

---

Latex:

---

Latex:

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


By

---

Latex:
(RW  (AddrC  [2]  (UnfoldC  `es-interface-predecessors`))  0
  THEN  Unfold  `eclass-events`  0
  THEN  Unfold  `es-le-before`  0
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto)

---

Home Index