---

Step * 4 of Lemma cp-ktype_wf


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
BY
{ ((GenConclAtAddr [2;1] THENA (DVar `i' THEN Auto)) THEN (RepeatFor 5 (D (-2)) THEN Reduce 0) THEN Auto)⋅ }

---

Latex:



1.  cp  :  i:Id  fp->  A:Type
                                    \mtimes{}  ks:\{k:Knd|  \muparrow{}hasloc(k;i)\}    List
                                    \mtimes{}  typ:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  Type
                                    \mtimes{}  k:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  (typ  k)  {}\mrightarrow{}  A  {}\mrightarrow{}  (Top  +  Top)
                                    \mtimes{}  A  {}\mrightarrow{}  k:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  (typ  k)  {}\mrightarrow{}  A
                                    \mtimes{}  A
2.  i  :  \{i:Id|  (i  \mmember{}  fpf-domain(cp))\} 
3.  \mcap{}k:\{k:Knd|  (k  \mmember{}  (\mlambda{}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  \mmember{}  Type)
4.  k  :  Knd@i
\mvdash{}  let  A,ks,typ,h,acc,init  =  cp(i)  in 
    ks  \mmember{}  Knd  List


By

((GenConclAtAddr  [2;1]  THENA  (DVar  `i'  THEN  Auto))
  THEN  (RepeatFor  5  (D  (-2))  THEN  Reduce  0)
  THEN  Auto)\mcdot{}

---

Home Index