---

Step * of Lemma cp-ktype_wf

∀[cp:ClassProgram(Top)]. ∀[i:{i:Id| (i ∈ cp-domain(cp))} ]. ∀[k:{k:Knd| (k ∈ cp-kinds(cp) i)} ].
  (cp-ktype(cp;i;k) ∈ Type)
BY
{ (Unfolds ``class-program cp-domain cp-kinds cp-ktype`` 0 THEN Auto) }

1
1. cp : i:Id fp-> A:Type
                  × ks:{k:Knd| ↑hasloc(k;i)}  List
                  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
                  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
                  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
                  × A
2. i : {i:Id| (i ∈ fpf-domain(cp))} 
3. k : {k:Knd| (k ∈ (λi.let A,ks,typ,h,acc,init = cp(i) in ks) i)} 
⊢ let A,ks,typ,h,acc,init = cp(i) in 
  typ k ∈ Type

2
1. cp : i:Id fp-> A:Type
                  × ks:{k:Knd| ↑hasloc(k;i)}  List
                  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
                  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
                  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
                  × A
2. i : {i:Id| (i ∈ fpf-domain(cp))} 
3. k : Knd@i
⊢ let A,ks,typ,h,acc,init = cp(i) in 
  ks ∈ Knd List

3
1. cp : i:Id fp-> A:Type
                  × ks:{k:Knd| ↑hasloc(k;i)}  List
                  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
                  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
                  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
                  × A
2. i : {i:Id| (i ∈ fpf-domain(cp))} 
3. ∩k:{k:Knd| (k ∈ (λi.let A,ks,typ,h,acc,init = cp(i) in ks) i)} . (let A,ks,typ,h,acc,init = cp(i) in typ k ∈ Type)
4. k : Knd@i
⊢ let A,ks,typ,h,acc,init = cp(i) in 
  ks ∈ Knd List

4
1. cp : i:Id fp-> A:Type
                  × ks:{k:Knd| ↑hasloc(k;i)}  List
                  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
                  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
                  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
                  × A
2. i : {i:Id| (i ∈ fpf-domain(cp))} 
3. ∩k:{k:Knd| (k ∈ (λi.let A,ks,typ,h,acc,init = cp(i) in ks) i)} . (let A,ks,typ,h,acc,init = cp(i) in typ k ∈ Type)
4. k : Knd@i
⊢ let A,ks,typ,h,acc,init = cp(i) in 
  ks ∈ Knd List

---

Latex:


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


By

(Unfolds  ``class-program  cp-domain  cp-kinds  cp-ktype``  0  THEN  Auto)

---

Home Index