---

Step * of Lemma cp-state-type_wf

∀[cp:ClassProgram(Top)]. ∀[i:Id].  (cp-state-type(cp;i) ∈ Type)
BY
{ (Unfolds ``class-program cp-domain cp-state-type`` 0
   THEN Auto
   THEN Try ((Fold `ifthenelse` (-1) THEN Fold `assert` (-1)))
   THEN GenConclAtAddr [2;1]
   THEN RepeatFor 5 (D -2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[cp:ClassProgram(Top)].  \mforall{}[i:Id].    (cp-state-type(cp;i)  \mmember{}  Type)


By

(Unfolds  ``class-program  cp-domain  cp-state-type``  0
  THEN  Auto
  THEN  Try  ((Fold  `ifthenelse`  (-1)  THEN  Fold  `assert`  (-1)))
  THEN  GenConclAtAddr  [2;1]
  THEN  RepeatFor  5  (D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index