---

Step * 1 of Lemma member-rcvs-on


1. tg : Id@i
2. links : IdLnk List@i
3. k : Knd@i
⊢ (k ∈ Rcvs(tg) on links) ⇐⇒ (↑isrcv(k)) ∧ (tag(k) = tg ∈ Id) ∧ (lnk(k) ∈ links)
BY
{ (Unfold `rcvs-on` 0 THEN (RWO "member_map" 0 THENA Auto)) }

1
1. tg : Id@i
2. links : IdLnk List@i
3. k : Knd@i
⊢ ∃y:IdLnk. ((y ∈ links) ∧ (k = ((λl.rcv(l,tg)) y) ∈ Knd)) ⇐⇒ (↑isrcv(k)) ∧ (tag(k) = tg ∈ Id) ∧ (lnk(k) ∈ links)

---

Latex:



1.  tg  :  Id@i
2.  links  :  IdLnk  List@i
3.  k  :  Knd@i
\mvdash{}  (k  \mmember{}  Rcvs(tg)  on  links)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}isrcv(k))  \mwedge{}  (tag(k)  =  tg)  \mwedge{}  (lnk(k)  \mmember{}  links)


By

(Unfold  `rcvs-on`  0  THEN  (RWO  "member\_map"  0  THENA  Auto))

---

Home Index