---

Step * 2 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 : Knd@i
⊢ let A,ks,typ,h,acc,init = cp(i) in 
  ks ∈ Knd List
BY
{ D -2
THEN ( (GenConclAtAddr [2;1])⋅ THENA Auto 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 : Id
3. (i ∈ fpf-domain(cp))
4. k : Knd@i
5. v : 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@i'
6. cp(i)
= v
∈ (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)@i'
⊢ let A,ks,typ,h,acc,init = v in 
  ks ∈ Knd List

---

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.  k  :  Knd@i
\mvdash{}  let  A,ks,typ,h,acc,init  =  cp(i)  in 
    ks  \mmember{}  Knd  List


By

D  -2
THEN  (  (GenConclAtAddr  [2;1])\mcdot{}  THENA  Auto  THEN  Auto)\mcdot{}

---

Home Index