---

Step * of Lemma primed-class-opt-cases2

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[b:Top]. ∀[e:E].
  (Prior(X)?b(e) ~ if first(e) then b loc(e)
  if 0 <z #(X(pred(e))) then X(pred(e))
  else Prior(X)?b(pred(e))
  fi )
BY
{ (RepUR ``class-ap`` 0 THEN InstLemma `primed-class-opt-cases` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[b:Top].  \mforall{}[e:E].
    (Prior(X)?b(e)  \msim{}  if  first(e)  then  b  loc(e)
    if  0  <z  \#(X(pred(e)))  then  X(pred(e))
    else  Prior(X)?b(pred(e))
    fi  )


By

---

Latex:
(RepUR  ``class-ap``  0  THEN  InstLemma  `primed-class-opt-cases`  []  THEN  Trivial)

---

Home Index