---

Step * 1 1 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
7. (lnk(k) ∈ links)
⊢ k = rcv(lnk(k),tag(k)) ∈ Knd
BY
{ DVar `k' }

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

2
1. tg : Id@i
2. links : IdLnk List@i
3. y : Id@i
4. ↑isrcv(inr y )@i
5. tag(inr y ) = tg ∈ Id@i
6. (lnk(inr y ) ∈ links)@i
7. (lnk(inr y ) ∈ links)
⊢ (inr y ) = rcv(lnk(inr y ),tag(inr y )) ∈ 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
7.  (lnk(k)  \mmember{}  links)
\mvdash{}  k  =  rcv(lnk(k),tag(k))


By

DVar  `k'

---

Home Index