---

Step * of Lemma primed-class-pred

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  Prior(X) es e ~ if 0 <z #(X es pred(e)) then X es pred(e) else Prior(X) es pred(e) fi  supposing ¬↑first(e)
BY
{ (InstLemma `primed-class-cases` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN SplitOnHypITE -2 
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `primed-class-cases`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  SplitOnHypITE  -2 
  THEN  Auto)

---

Home Index