---

Step * 1 of Lemma graph-rcvs_wf


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
BY
{ Assert ⌈S ∈ {j:Id| (j ∈ S)}  List⌉⋅ }

1
.....assertion..... 
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)} 
⊢ S ∈ {j:Id| (j ∈ S)}  List

2
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)} 
6. S ∈ {j:Id| (j ∈ S)}  List
⊢ mapfilter(λi.rcv((link(a i j) from i to j),b);λi.j ∈b G i);S) ∈ Knd List

---

Latex:



1.  S  :  Id  List
2.  G  :  \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  (\{i:Id|  (i  \mmember{}  S)\}    List)
3.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id
4.  b  :  Id
5.  j  :  \{j:Id|  (j  \mmember{}  S)\} 
\mvdash{}  mapfilter(\mlambda{}i.rcv((link(a  i  j)  from  i  to  j),b);\mlambda{}i.j  \mmember{}\msubb{}  G  i);S)  \mmember{}  Knd  List


By

Assert  \mkleeneopen{}S  \mmember{}  \{j:Id|  (j  \mmember{}  S)\}    List\mkleeneclose{}\mcdot{}

---

Home Index