---

Step * 1 2 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) ∧ (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))
BY
{ (With ⌈map(λv.(link(tg) from v to destination(l));srclocs)⌉ (D 0)⋅ THEN Auto) }

1
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
⊢ ∃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)))

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
6. ∃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)))
⊢ (l ∈ map(λv.(link(tg) from v to destination(l));srclocs))

---

Latex:



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


By

(With  \mkleeneopen{}map(\mlambda{}v.(link(tg)  from  v  to  destination(l));srclocs)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index