---

Step * of Lemma member-links-from-to

∀tg:Id. ∀srclocs,dstlocs:Id List. ∀l:IdLnk.
  ((l ∈ links(tg) from srclocs to dstlocs)
  ⇐⇒ {(source(l) ∈ srclocs) ∧ (destination(l) ∈ dstlocs) ∧ (lname(l) = tg ∈ Id)})
BY
{ ((UnivCD THENA Auto) THEN Unfold `links-from-to` 0) }

1
1. tg : Id@i
2. srclocs : Id List@i
3. dstlocs : Id List@i
4. l : IdLnk@i
⊢ (l ∈ concat(map(λc.map(λv.(link(tg) from v to c);srclocs);dstlocs)))
⇐⇒ {(source(l) ∈ srclocs) ∧ (destination(l) ∈ dstlocs) ∧ (lname(l) = tg ∈ Id)}

---

Latex:


\mforall{}tg:Id.  \mforall{}srclocs,dstlocs:Id  List.  \mforall{}l:IdLnk.
    ((l  \mmember{}  links(tg)  from  srclocs  to  dstlocs)
    \mLeftarrow{}{}\mRightarrow{}  \{(source(l)  \mmember{}  srclocs)  \mwedge{}  (destination(l)  \mmember{}  dstlocs)  \mwedge{}  (lname(l)  =  tg)\})


By

((UnivCD  THENA  Auto)  THEN  Unfold  `links-from-to`  0)

---

Home Index