---

Step * 3 of Lemma lnk-decl_wf-hasloc


1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. ∀k:Knd. (↑hasloc(k;destination(l)) ∈ Type)
4. k : Knd
5. ↑hasloc(k;destination(l))
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.  \mforall{}k:Knd.  (\muparrow{}hasloc(k;destination(l))  \mmember{}  Type)
4.  k  :  Knd
5.  \muparrow{}hasloc(k;destination(l))
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{})

---

Home Index