---

Step * 1 1 of Lemma locknd_functionality_isrcv


1. i : Id
2. j : Id
3. k1 : Knd
4. k2 : Knd
5. ↑isrcv(k1)
6. k1 = k2 ∈ Knd
7. k1 = rcv(lnk(k1),tag(k1)) ∈ Knd
⊢ ↑hasloc(rcv(lnk(k1),tag(k1));destination(lnk(k1)))
BY
{ (((RWO "assert-hasloc" 0 THEN Auto) THEN Reduce 0) THEN Auto) }

---

Latex:



1.  i  :  Id
2.  j  :  Id
3.  k1  :  Knd
4.  k2  :  Knd
5.  \muparrow{}isrcv(k1)
6.  k1  =  k2
7.  k1  =  rcv(lnk(k1),tag(k1))
\mvdash{}  \muparrow{}hasloc(rcv(lnk(k1),tag(k1));destination(lnk(k1)))


By

(((RWO  "assert-hasloc"  0  THEN  Auto)  THEN  Reduce  0)  THEN  Auto)

---

Home Index