---

Step * of Lemma graph-rcvs_wf2

∀[S:Id List]. ∀[G:Graph(S)]. ∀[a:Id ⟶ Id ⟶ Id]. ∀[b:Id]. ∀[j:{j:Id| (j ∈ S)} ].
  (graph-rcvs(S;G;a;b;j) ∈ {k:Knd| ↑hasloc(k;j)}  List)
BY
{ (Auto
   THEN GenConcl ⌜graph-rcvs(S;G;a;b;j) = L ∈ ({k:Knd| (k ∈ graph-rcvs(S;G;a;b;j))}  List)⌝⋅
   THEN Auto
   THEN DoSubsume
   THEN Auto
   THEN SubtypeReasoning
   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. (x ∈ graph-rcvs(S;G;a;b;j))@i
⊢ ↑hasloc(x;j)

---

Latex:

---

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)\}  ].
    (graph-rcvs(S;G;a;b;j)  \mmember{}  \{k:Knd|  \muparrow{}hasloc(k;j)\}    List)


By

---

Latex:
(Auto
  THEN  GenConcl  \mkleeneopen{}graph-rcvs(S;G;a;b;j)  =  L\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto
  THEN  SubtypeReasoning
  THEN  Auto)

---

Home Index