---

Step * 1 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. l1 : IdLnk List@i
6. y : Id@i
7. (y ∈ dstlocs)@i
8. l1 = map(λv.(link(tg) from v to y);srclocs) ∈ (IdLnk List)@i
9. (l ∈ l1)@i
⊢ (source(l) ∈ srclocs) ∧ (destination(l) ∈ dstlocs) ∧ (lname(l) = tg ∈ Id)
BY
{ (HypSubst' (-2) (-1) THEN ((RWO "member_map" (-1) THENM (Reduce (-1) THEN ExRepD)) THENA Auto)) }

1
1. tg : Id@i
2. srclocs : Id List@i
3. dstlocs : Id List@i
4. l : IdLnk@i
5. l1 : IdLnk List@i
6. y : Id@i
7. (y ∈ dstlocs)@i
8. l1 = map(λv.(link(tg) from v to y);srclocs) ∈ (IdLnk List)@i
9. y1 : Id
10. (y1 ∈ srclocs)
11. l = (link(tg) from y1 to y) ∈ IdLnk
⊢ (source(l) ∈ srclocs) ∧ (destination(l) ∈ dstlocs) ∧ (lname(l) = tg ∈ Id)

---

Latex:



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


By

(HypSubst'  (-2)  (-1)  THEN  ((RWO  "member\_map"  (-1)  THENM  (Reduce  (-1)  THEN  ExRepD))  THENA  Auto))

---

Home Index