---

Step * 1 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. 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)
BY
{ (RepUR ``hasloc`` 0 THEN RW assert_pushdownC 0 THEN Auto) }

---

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.  i  :  Id
11.  (i  \mmember{}  S)
12.  (i{}\mrightarrow{}j)\mmember{}G
13.  x  =  rcv((link(a  i  j)  from  i  to  j),b)
\mvdash{}  \muparrow{}hasloc(rcv((link(a  i  j)  from  i  to  j),b);j)


By

(RepUR  ``hasloc``  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index