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