---

Step * 1 of Lemma id-graph-edge-implies-member


1. S : Id List@i
2. G : Graph(S)@i
3. i : {i:Id| (i ∈ S)} @i
4. j : Id@i
5. (j ∈ G i)@i
⊢ (j ∈ S)
BY
{ (RepeatFor 2 (D (-1)) THEN HypSubst' -1 0) }

1
1. S : Id List@i
2. G : Graph(S)@i
3. i : {i:Id| (i ∈ S)} @i
4. j : Id@i
5. i@0 : ℕ@i
6. i@0 < ||G i||@i
7. j = G i[i@0] ∈ Id@i
⊢ (G i[i@0] ∈ S)

---

Latex:

---

Latex:

1.  S  :  Id  List@i
2.  G  :  Graph(S)@i
3.  i  :  \{i:Id|  (i  \mmember{}  S)\}  @i
4.  j  :  Id@i
5.  (j  \mmember{}  G  i)@i
\mvdash{}  (j  \mmember{}  S)


By

---

Latex:
(RepeatFor  2  (D  (-1))  THEN  HypSubst'  -1  0)

---

Home Index