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