---

Step * 1 2 2 1 of Lemma member-links-from-to


1. tg : Id@i
2. srclocs : Id List@i
3. dstlocs : Id List@i
4. l : IdLnk@i
5. (source(l) ∈ srclocs)@i
6. (destination(l) ∈ dstlocs)@i
7. lname(l) = tg ∈ Id@i
8. ∃y:Id
    ((y ∈ dstlocs)
    ∧ (map(λv.(link(tg) from v to destination(l));srclocs) = map(λv.(link(tg) from v to y);srclocs) ∈ (IdLnk List)))
9. (source(l) ∈ srclocs)
⊢ l = (link(tg) from source(l) to destination(l)) ∈ IdLnk
BY
{ (RepeatFor 2 (D -6) THEN All Reduce THEN Fold `mk_lnk` 0 THEN EqCD THEN Auto) }

---

Latex:



1.  tg  :  Id@i
2.  srclocs  :  Id  List@i
3.  dstlocs  :  Id  List@i
4.  l  :  IdLnk@i
5.  (source(l)  \mmember{}  srclocs)@i
6.  (destination(l)  \mmember{}  dstlocs)@i
7.  lname(l)  =  tg@i
8.  \mexists{}y:Id
        ((y  \mmember{}  dstlocs)
        \mwedge{}  (map(\mlambda{}v.(link(tg)  from  v  to  destination(l));srclocs)
            =  map(\mlambda{}v.(link(tg)  from  v  to  y);srclocs)))
9.  (source(l)  \mmember{}  srclocs)
\mvdash{}  l  =  (link(tg)  from  source(l)  to  destination(l))


By

(RepeatFor  2  (D  -6)  THEN  All  Reduce  THEN  Fold  `mk\_lnk`  0  THEN  EqCD  THEN  Auto)

---

Home Index