---

Step * 1 1 1 of Lemma member-rcvs-on


1. tg : Id@i
2. links : IdLnk List@i
3. k : Knd@i
4. ↑isrcv(k)@i
5. tag(k) = tg ∈ Id@i
6. (lnk(k) ∈ links)@i
⊢ ∃y:IdLnk. ((y ∈ links) ∧ (k = rcv(y,tg) ∈ Knd))
BY
{ (With ⌈lnk(k)⌉ (D 0)⋅ THEN Auto) }

1
1. tg : Id@i
2. links : IdLnk List@i
3. k : Knd@i
4. ↑isrcv(k)@i
5. tag(k) = tg ∈ Id@i
6. (lnk(k) ∈ links)@i
7. (lnk(k) ∈ links)
⊢ k = rcv(lnk(k),tg) ∈ Knd

---

Latex:



1.  tg  :  Id@i
2.  links  :  IdLnk  List@i
3.  k  :  Knd@i
4.  \muparrow{}isrcv(k)@i
5.  tag(k)  =  tg@i
6.  (lnk(k)  \mmember{}  links)@i
\mvdash{}  \mexists{}y:IdLnk.  ((y  \mmember{}  links)  \mwedge{}  (k  =  rcv(y,tg)))


By

(With  \mkleeneopen{}lnk(k)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index