---

Step * 1 1 1 1 1 1 of Lemma member-rcvs-on


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
BY
{ (DVar `x' THEN All (Fold `rcv`) THEN Reduce 0 THEN Auto) }

---

Latex:



1.  tg  :  Id@i
2.  links  :  IdLnk  List@i
3.  x  :  IdLnk  \mtimes{}  Id@i
4.  \muparrow{}isrcv(inl  x)@i
5.  tag(inl  x)  =  tg@i
6.  (lnk(inl  x)  \mmember{}  links)@i
7.  (lnk(inl  x)  \mmember{}  links)
\mvdash{}  (inl  x)  =  rcv(lnk(inl  x),tag(inl  x))


By

(DVar  `x'  THEN  All  (Fold  `rcv`)  THEN  Reduce  0  THEN  Auto)

---

Home Index