---

Step * 1 of Lemma rcvs-on-links-from-to


1. tg1 : Id@i
2. tg2 : Id@i
3. srclocs : Id List@i
4. dstlocs : Id List@i
5. d : Id@i
6. (d ∈ dstlocs)@i
7. s : Id@i
8. (s ∈ srclocs)@i
⊢ (rcv((link(tg2) from s to d),tg1) ∈ Rcvs(tg1) on links(tg2) from srclocs to dstlocs)
BY
{ Assert ⌈(rcv((link(tg2) from s to d),tg1) ∈ Rcvs(tg1) on links(tg2) from srclocs to dstlocs)⌉⋅ }

1
.....assertion..... 
1. tg1 : Id@i
2. tg2 : Id@i
3. srclocs : Id List@i
4. dstlocs : Id List@i
5. d : Id@i
6. (d ∈ dstlocs)@i
7. s : Id@i
8. (s ∈ srclocs)@i
⊢ (rcv((link(tg2) from s to d),tg1) ∈ Rcvs(tg1) on links(tg2) from srclocs to dstlocs)

2
1. tg1 : Id@i
2. tg2 : Id@i
3. srclocs : Id List@i
4. dstlocs : Id List@i
5. d : Id@i
6. (d ∈ dstlocs)@i
7. s : Id@i
8. (s ∈ srclocs)@i
9. (rcv((link(tg2) from s to d),tg1) ∈ Rcvs(tg1) on links(tg2) from srclocs to dstlocs)
⊢ (rcv((link(tg2) from s to d),tg1) ∈ Rcvs(tg1) on links(tg2) from srclocs to dstlocs)

---

Latex:



1.  tg1  :  Id@i
2.  tg2  :  Id@i
3.  srclocs  :  Id  List@i
4.  dstlocs  :  Id  List@i
5.  d  :  Id@i
6.  (d  \mmember{}  dstlocs)@i
7.  s  :  Id@i
8.  (s  \mmember{}  srclocs)@i
\mvdash{}  (rcv((link(tg2)  from  s  to  d),tg1)  \mmember{}  Rcvs(tg1)  on  links(tg2)  from  srclocs  to  dstlocs)


By

Assert  \mkleeneopen{}(rcv((link(tg2)  from  s  to  d),tg1)  \mmember{}  Rcvs(tg1)  on  links(tg2)  from  srclocs  to  dstlocs)\mkleeneclose{}\mcdot{}

---

Home Index