---

Step * 2 of Lemma lnk-decl_wf-hasloc


1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. k : {k:{k:Knd| ↑hasloc(k;destination(l))} | (k ∈ map(λtg.rcv(l,tg);fst(dt)))} @i
⊢ dt(snd(outl(k))) ∈ Type
BY
{ (D -1 THEN D -2 THEN ((RWO "member_map" (-1)) THENA Auto)) }

1
1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. k : Knd@i
4. ↑hasloc(k;destination(l))@i
5. (k ∈ map(λtg.rcv(l,tg);fst(dt)))@i
6. tg : Id@i
⊢ rcv(l,tg) ∈ {k:Knd| ↑hasloc(k;destination(l))} 

2
1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. k : Knd@i
4. ↑hasloc(k;destination(l))@i
5. ∃y:Id. ((y ∈ fst(dt)) ∧ (k = ((λtg.rcv(l,tg)) y) ∈ {k:Knd| ↑hasloc(k;destination(l))} ))
⊢ dt(snd(outl(k))) ∈ Type

---

Latex:



1.  l  :  IdLnk
2.  dt  :  d:Id  List  \mtimes{}  (tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type)
3.  k  :  \{k:\{k:Knd|  \muparrow{}hasloc(k;destination(l))\}  |  (k  \mmember{}  map(\mlambda{}tg.rcv(l,tg);fst(dt)))\}  @i
\mvdash{}  dt(snd(outl(k)))  \mmember{}  Type


By

(D  -1  THEN  D  -2  THEN  ((RWO  "member\_map"  (-1))  THENA  Auto))

---

Home Index