---

Step * 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
⊢ (l ∈ concat(map(λc.map(λv.(link(tg) from v to c);srclocs);dstlocs)))
⇐⇒ {(source(l) ∈ srclocs) ∧ (destination(l) ∈ dstlocs) ∧ (lname(l) = tg ∈ Id)}
BY
{ ((RWW "member-concat member_map" 0 THENM Reduce 0) THEN Auto THEN ExRepD) }

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. (l ∈ l1)@i
⊢ (source(l) ∈ srclocs) ∧ (destination(l) ∈ dstlocs) ∧ (lname(l) = tg ∈ Id)

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

---

Latex:



1.  tg  :  Id@i
2.  srclocs  :  Id  List@i
3.  dstlocs  :  Id  List@i
4.  l  :  IdLnk@i
\mvdash{}  (l  \mmember{}  concat(map(\mlambda{}c.map(\mlambda{}v.(link(tg)  from  v  to  c);srclocs);dstlocs)))
\mLeftarrow{}{}\mRightarrow{}  \{(source(l)  \mmember{}  srclocs)  \mwedge{}  (destination(l)  \mmember{}  dstlocs)  \mwedge{}  (lname(l)  =  tg)\}


By

((RWW  "member-concat  member\_map"  0  THENM  Reduce  0)  THEN  Auto  THEN  ExRepD)

---

Home Index