---

Step * 1 of Lemma graph-rcvs_wf2


1. S : Id List
2. G : Graph(S)
3. a : Id ─→ Id ─→ Id
4. b : Id
5. j : {j:Id| (j ∈ S)} 
6. L : {k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List@i
7. graph-rcvs(S;G;a;b;j) = L ∈ ({k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List)@i
8. L = L ∈ ({k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List)
9. x : Knd@i
10. (x ∈ graph-rcvs(S;G;a;b;j))@i
⊢ ↑hasloc(x;j)
BY
{ ((RWO "member-graph-rcvs" (-1) THENM ExRepD THENM HypSubst' -1 0) THEN Auto) }

1
1. S : Id List
2. G : Graph(S)
3. a : Id ─→ Id ─→ Id
4. b : Id
5. j : {j:Id| (j ∈ S)} 
6. L : {k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List@i
7. graph-rcvs(S;G;a;b;j) = L ∈ ({k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List)@i
8. L = L ∈ ({k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List)
9. x : Knd@i
10. i : Id
11. (i ∈ S)
12. (i─→j)∈G
13. x = rcv((link(a i j) from i to j),b) ∈ Knd
⊢ ↑hasloc(rcv((link(a i j) from i to j),b);j)

---

Latex:



1.  S  :  Id  List
2.  G  :  Graph(S)
3.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id
4.  b  :  Id
5.  j  :  \{j:Id|  (j  \mmember{}  S)\} 
6.  L  :  \{k:Knd|  (k  \mmember{}  graph-rcvs(S;G;a;b;j))\}    List@i
7.  graph-rcvs(S;G;a;b;j)  =  L@i
8.  L  =  L
9.  x  :  Knd@i
10.  (x  \mmember{}  graph-rcvs(S;G;a;b;j))@i
\mvdash{}  \muparrow{}hasloc(x;j)


By

((RWO  "member-graph-rcvs"  (-1)  THENM  ExRepD  THENM  HypSubst'  -1  0)  THEN  Auto)

---

Home Index