---

Step * 1 1 1 of Lemma assert-graph-rcvset


1. a : Id ─→ Id ─→ Id@i
2. b : Id@i
3. S : Id List@i
4. G : {i:Id| (i ∈ S)}  ─→ ({i:Id| (i ∈ S)}  List)@i
5. x3 : Id@i
6. x5 : Id@i
7. x6 : Id@i
8. x2 : Id@i
9. (x3 ∈ S)
10. x2 = b ∈ Id
11. x6 = (a x3 x5) ∈ Id
12. (x3─→x5)∈G
13. (x3 ∈ S)
⊢ (x5 ∈ S)
BY
{ (UsingVars [`S'] (FLemma `id-graph-edge-implies-member` [-2]) THEN Auto) }

---

Latex:



1.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id@i
2.  b  :  Id@i
3.  S  :  Id  List@i
4.  G  :  \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  (\{i:Id|  (i  \mmember{}  S)\}    List)@i
5.  x3  :  Id@i
6.  x5  :  Id@i
7.  x6  :  Id@i
8.  x2  :  Id@i
9.  (x3  \mmember{}  S)
10.  x2  =  b
11.  x6  =  (a  x3  x5)
12.  (x3{}\mrightarrow{}x5)\mmember{}G
13.  (x3  \mmember{}  S)
\mvdash{}  (x5  \mmember{}  S)


By

(UsingVars  [`S']  (FLemma  `id-graph-edge-implies-member`  [-2])  THEN  Auto)

---

Home Index