---

Step * of Lemma member-graph-rcvs

∀S:Id List. ∀G:Graph(S). ∀a:Id ─→ Id ─→ Id. ∀b:Id. ∀j:{j:Id| (j ∈ S)} . ∀k:Knd.
  ((k ∈ graph-rcvs(S;G;a;b;j)) ⇐⇒ ∃i:Id. ((i ∈ S) ∧ (i─→j)∈G ∧ (k = rcv((link(a i j) from i to j),b) ∈ Knd)))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert S ∈ {j:Id| (j ∈ S)}  List BY
               Auto)
   THEN Unfold `id-graph` 2
   THEN ((Unfolds ``graph-rcvs id-graph-edge`` 0 THEN RWO  "member_map_filter" 0) THENA Try (Complete (Auto)))
   THEN Reduce 0
   THEN Auto
   THEN (ParallelLast THEN Auto)⋅) }

1
1. S : Id List@i
2. G : {i:Id| (i ∈ S)}  ─→ ({i:Id| (i ∈ S)}  List)@i
3. a : Id ─→ Id ─→ Id@i
4. b : Id@i
5. j : {j:Id| (j ∈ S)} @i
6. k : Knd@i
7. S ∈ {j:Id| (j ∈ S)}  List
8. y : {j:Id| (j ∈ S)} @i
9. (y ∈ S)@i
10. (↑j ∈b G y)) c∧ (k = rcv((link(a y j) from y to j),b) ∈ Knd)@i
11. (y ∈ S)
⊢ (j ∈ G y)

---

Latex:


\mforall{}S:Id  List.  \mforall{}G:Graph(S).  \mforall{}a:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id.  \mforall{}b:Id.  \mforall{}j:\{j:Id|  (j  \mmember{}  S)\}  .  \mforall{}k:Knd.
    ((k  \mmember{}  graph-rcvs(S;G;a;b;j))
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:Id.  ((i  \mmember{}  S)  \mwedge{}  (i{}\mrightarrow{}j)\mmember{}G  \mwedge{}  (k  =  rcv((link(a  i  j)  from  i  to  j),b))))


By

((UnivCD  THENA  Auto)
  THEN  (Assert  S  \mmember{}  \{j:Id|  (j  \mmember{}  S)\}    List  BY
                          Auto)
  THEN  Unfold  `id-graph`  2
  THEN  ((Unfolds  ``graph-rcvs  id-graph-edge``  0  THEN  RWO    "member\_map\_filter"  0)
              THENA  Try  (Complete  (Auto))
              )
  THEN  Reduce  0
  THEN  Auto
  THEN  (ParallelLast  THEN  Auto)\mcdot{})

---

Home Index