---

Step * 1 1 of Lemma member-graph-rcvs


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)@i
11. k = rcv((link(a y j) from y to j),b) ∈ Knd@i
12. (y ∈ S)
⊢ (j ∈ G y)
BY
{ (RW assert_pushdownC (-3) THEN Auto) }

---

Latex:



1.  S  :  Id  List@i
2.  G  :  \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  (\{i:Id|  (i  \mmember{}  S)\}    List)@i
3.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id@i
4.  b  :  Id@i
5.  j  :  \{j:Id|  (j  \mmember{}  S)\}  @i
6.  k  :  Knd@i
7.  S  \mmember{}  \{j:Id|  (j  \mmember{}  S)\}    List
8.  y  :  \{j:Id|  (j  \mmember{}  S)\}  @i
9.  (y  \mmember{}  S)@i
10.  \muparrow{}j  \mmember{}\msubb{}  G  y)@i
11.  k  =  rcv((link(a  y  j)  from  y  to  j),b)@i
12.  (y  \mmember{}  S)
\mvdash{}  (j  \mmember{}  G  y)


By

(RW  assert\_pushdownC  (-3)  THEN  Auto)

---

Home Index