---

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

∀tg1,tg2:Id. ∀srclocs,dstlocs:Id List.
  (∀d∈dstlocs.(∀s∈srclocs.(∃k∈Rcvs(tg1) on links(tg2) from srclocs to dstlocs. (source(lnk(k)) = s ∈ Id)
                 ∧ (destination(lnk(k)) = d ∈ Id))))
BY
{ (Auto
   THEN RWW "l_all_iff l_exists_iff" 0
   THEN Auto
   THEN Try (Complete ((RepeatFor 2 (DVar `k') THEN Auto)))
   THEN With ⌈rcv((link(tg2) from s to d),tg1)⌉ (D 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
⊢ (rcv((link(tg2) from s to d),tg1) ∈ Rcvs(tg1) on links(tg2) from srclocs to dstlocs)

---

Latex:


\mforall{}tg1,tg2:Id.  \mforall{}srclocs,dstlocs:Id  List.
    (\mforall{}d\mmember{}dstlocs.(\mforall{}s\mmember{}srclocs.(\mexists{}k\mmember{}Rcvs(tg1)  on  links(tg2)  from  srclocs  to  dstlocs.  (source(lnk(k))  =  s)
                                  \mwedge{}  (destination(lnk(k))  =  d))))


By

(Auto
  THEN  RWW  "l\_all\_iff  l\_exists\_iff"  0
  THEN  Auto
  THEN  Try  (Complete  ((RepeatFor  2  (DVar  `k')  THEN  Auto)))
  THEN  With  \mkleeneopen{}rcv((link(tg2)  from  s  to  d),tg1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index