Step
*
1
1
of Lemma
rcvs-on-links-from-to
.....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)
BY
{ (RWW "member-rcvs-on member-links-from-to" 0 THEN Auto) }
1
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. ↑isrcv(rcv((link(tg2) from s to d),tg1))
10. tag(rcv((link(tg2) from s to d),tg1)) = tg1 ∈ Id
⊢ {(source(lnk(rcv((link(tg2) from s to d),tg1))) ∈ srclocs)
∧ (destination(lnk(rcv((link(tg2) from s to d),tg1))) ∈ dstlocs)
∧ (lname(lnk(rcv((link(tg2) from s to d),tg1))) = tg2 ∈ Id)}
Latex:
.....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 \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
(RWW "member-rcvs-on member-links-from-to" 0 THEN Auto)
Home
Index