---

Step * 1 of Lemma es-le-interface-val-cases


∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.  (le(X)(e) ~ if e ∈b X then e else prior(X)(e) fi )
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN RepUR ``es-le-interface es-prior-interface local-pred-class`` 0
   THEN RepUR ``in-eclass eclass-val can-apply do-apply`` 0⋅
   THEN Unfold `eclass` -1
   THEN CausalInd'
   THEN (RecUnfold `es-local-le-pred` 0 THEN Reduce 0)
   THEN RecUnfold `es-local-pred` 0
   THEN Reduce 0
   THEN RepeatFor 2 (OldAutoSplit)
   THEN (RWO "-3" 0 THENM Try (OldAutoSplit))
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.    (le(X)(e)  \msim{}  if  e  \mmember{}\msubb{}  X  then  e  else  prior(X)(e)  fi  )


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  RepUR  ``es-le-interface  es-prior-interface  local-pred-class``  0
  THEN  RepUR  ``in-eclass  eclass-val  can-apply  do-apply``  0\mcdot{}
  THEN  Unfold  `eclass`  -1
  THEN  CausalInd'
  THEN  (RecUnfold  `es-local-le-pred`  0  THEN  Reduce  0)
  THEN  RecUnfold  `es-local-pred`  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (OldAutoSplit)
  THEN  (RWO  "-3"  0  THENM  Try  (OldAutoSplit))
  THEN  Auto)

---

Home Index