---

Step * of Lemma locknd_functionality_isrcv

∀[i,j:Id]. ∀[k1,k2:Knd].  (locknd(i;k1) = locknd(j;k2) ∈ LocKnd) supposing ((k1 = k2 ∈ Knd) and (↑isrcv(k1)))
BY
{ (Auto THEN RevHypSubst' -1 0 THEN (FLemma `isrcv-implies` [-2] THENA Auto) THEN HypSubst' -1 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
⊢ locknd(i;rcv(lnk(k1),tag(k1))) = locknd(j;rcv(lnk(k1),tag(k1))) ∈ LocKnd

---

Latex:


\mforall{}[i,j:Id].  \mforall{}[k1,k2:Knd].    (locknd(i;k1)  =  locknd(j;k2))  supposing  ((k1  =  k2)  and  (\muparrow{}isrcv(k1)))


By

(Auto  THEN  RevHypSubst'  -1  0  THEN  (FLemma  `isrcv-implies`  [-2]  THENA  Auto)  THEN  HypSubst'  -1  0)

---

Home Index