---

Step * 2 1 of Lemma lnk-decl_wf-hasloc


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))} 
BY
{ (MemTypeCD
   THEN Auto
   THEN (RepUR ``hasloc`` 0 THEN RW assert_pushdownC 0 THEN Auto THEN (D 0 THEN Auto) THEN D -1 THEN Auto)⋅)⋅ }

---

Latex:



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


By

(MemTypeCD
  THEN  Auto
  THEN  (RepUR  ``hasloc``  0
              THEN  RW  assert\_pushdownC  0
              THEN  Auto
              THEN  (D  0  THEN  Auto)
              THEN  D  -1
              THEN  Auto)\mcdot{})\mcdot{}

---

Home Index