---

Step * 1 of Lemma prior-val-cases


∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.
  ((X)' es e ~ if first(e) then {}
  if pred(e) ∈b X then {X(pred(e))}
  else (X)' es pred(e)
  fi )
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN RepUR ``es-prior-val es-prior-interface local-pred-class in-eclass`` 0
   THEN RepUR ``eclass-val`` 0
   THEN Unfold `eclass` -1
   THEN CausalInd'
   THEN RW (AddrC [1] (RecUnfoldC `es-local-pred`)) 0
   THEN Reduce 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  RepUR  ``es-prior-val  es-prior-interface  local-pred-class  in-eclass``  0
  THEN  RepUR  ``eclass-val``  0
  THEN  Unfold  `eclass`  -1
  THEN  CausalInd'
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `es-local-pred`))  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index