---

Step * 1 1 of Lemma graph-rcvs_wf

.....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
BY
{ Auto }

---

Latex:


.....assertion..... 
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{}  S  \mmember{}  \{j:Id|  (j  \mmember{}  S)\}    List


By

Auto

---

Home Index