---

Step * of Lemma primed-class-opt-cases

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[b:Top]. ∀[e:E].
  (Prior(X)?b es e ~ if first(e) then b loc(e)
  if 0 <z #(X es pred(e)) then X es pred(e)
  else Prior(X)?b es pred(e)
  fi )
BY
{ (Auto
   THEN RepUR ``primed-class-opt local-pred-class`` 0
   THEN MoveToConcl (-1)
   THEN Unfold `eclass` -2
   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{}[b:Top].  \mforall{}[e:E].
    (Prior(X)?b  es  e  \msim{}  if  first(e)  then  b  loc(e)
    if  0  <z  \#(X  es  pred(e))  then  X  es  pred(e)
    else  Prior(X)?b  es  pred(e)
    fi  )


By

---

Latex:
(Auto
  THEN  RepUR  ``primed-class-opt  local-pred-class``  0
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `eclass`  -2
  THEN  CausalInd'
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `es-local-pred`))  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index