---

Step * of Lemma member-rcvs-on

∀tg:Id. ∀links:IdLnk List. ∀k:Knd.  ((k ∈ Rcvs(tg) on links) ⇐⇒ (↑isrcv(k)) ∧ (tag(k) = tg ∈ Id) ∧ (lnk(k) ∈ links))
BY
{ (UnivCD THENA Auto) }

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

---

Latex:


\mforall{}tg:Id.  \mforall{}links:IdLnk  List.  \mforall{}k:Knd.
    ((k  \mmember{}  Rcvs(tg)  on  links)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}isrcv(k))  \mwedge{}  (tag(k)  =  tg)  \mwedge{}  (lnk(k)  \mmember{}  links))


By

(UnivCD  THENA  Auto)

---

Home Index