---

Step * 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
⊢ locknd(i;rcv(lnk(k1),tag(k1))) = locknd(j;rcv(lnk(k1),tag(k1))) ∈ LocKnd
BY
{ ((RepUR ``locknd kindcase rcv islocal lnk`` 0 THEN Folds ``lnk rcv`` 0) THEN EqTypeCD THEN Auto THEN Reduce 0) }

1
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)))

---

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{}  locknd(i;rcv(lnk(k1),tag(k1)))  =  locknd(j;rcv(lnk(k1),tag(k1)))


By

((RepUR  ``locknd  kindcase  rcv  islocal  lnk``  0  THEN  Folds  ``lnk  rcv``  0)
  THEN  EqTypeCD
  THEN  Auto
  THEN  Reduce  0)

---

Home Index