---

Step * of Lemma cp-test_wf

∀[T:Type]. ∀[cp:ClassProgram(T)]. ∀[i:{i:Id| (i ∈ cp-domain(cp))} ].
  (cp-test(cp;i) ∈ k:{k:Knd| (k ∈ cp-kinds(cp) i)}  ─→ cp-ktype(cp;i;k) ─→ cp-state-type(cp;i) ─→ (T + Top))
BY
{ (Unfolds ``class-program cp-domain cp-test cp-ktype cp-kinds cp-state-type`` 0
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN D -1
   THEN (GenConclAtAddr [2;1] THENA Auto)
   THEN (RepeatFor 5 (D -2) THEN Reduce 0)
   THEN Subst' i ∈ dom(cp) ~ tt 0
   THEN Auto) }

---

Latex:


\mforall{}[T:Type].  \mforall{}[cp:ClassProgram(T)].  \mforall{}[i:\{i:Id|  (i  \mmember{}  cp-domain(cp))\}  ].
    (cp-test(cp;i)  \mmember{}  k:\{k:Knd|  (k  \mmember{}  cp-kinds(cp)  i)\} 
      {}\mrightarrow{}  cp-ktype(cp;i;k)
      {}\mrightarrow{}  cp-state-type(cp;i)
      {}\mrightarrow{}  (T  +  Top))


By

(Unfolds  ``class-program  cp-domain  cp-test  cp-ktype  cp-kinds  cp-state-type``  0
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  D  -1
  THEN  (GenConclAtAddr  [2;1]  THENA  Auto)
  THEN  (RepeatFor  5  (D  -2)  THEN  Reduce  0)
  THEN  Subst'  i  \mmember{}  dom(cp)  \msim{}  tt  0
  THEN  Auto)

---

Home Index