---

Step * of Lemma graph-rcvs_wf

∀[S:Id List]. ∀[G:Graph(S)]. ∀[a:Id ─→ Id ─→ Id]. ∀[b:Id]. ∀[j:{j:Id| (j ∈ S)} ].  (graph-rcvs(S;G;a;b;j) ∈ Knd List)
BY
{ (Auto THEN All (Unfolds ``id-graph graph-rcvs``)) }

1
1. S : Id List
2. G : {i:Id| (i ∈ S)}  ─→ ({i:Id| (i ∈ S)}  List)
3. a : Id ─→ Id ─→ Id
4. b : Id
5. j : {j:Id| (j ∈ S)} 
⊢ mapfilter(λi.rcv((link(a i j) from i to j),b);λi.j ∈b G i);S) ∈ Knd List

---

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{}  Knd  List)


By

(Auto  THEN  All  (Unfolds  ``id-graph  graph-rcvs``))

---

Home Index