---

Step * 1 1 of Lemma member-rcvs-on


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)
BY
{ (Reduce 0 THEN Auto THEN ExRepD THEN Try ((SubstFor ⌈k⌉ 0⋅ THEN Reduce 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
⊢ ∃y:IdLnk. ((y ∈ links) ∧ (k = rcv(y,tg) ∈ Knd))

---

Latex:



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


By

(Reduce  0  THEN  Auto  THEN  ExRepD  THEN  Try  ((SubstFor  \mkleeneopen{}k\mkleeneclose{}  0\mcdot{}  THEN  Reduce  0  THEN  Auto)))

---

Home Index