---

Step * 1 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. i@0 : ℕ@i
6. i@0 < ||G i||@i
7. j = G i[i@0] ∈ Id@i
⊢ (G i[i@0] ∈ S)
BY
{ (Unfold `id-graph` 2 THEN GenConclAtAddr [1] THEN Auto) }

---

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.  i@0  :  \mBbbN{}@i
6.  i@0  <  ||G  i||@i
7.  j  =  G  i[i@0]@i
\mvdash{}  (G  i[i@0]  \mmember{}  S)


By

---

Latex:
(Unfold  `id-graph`  2  THEN  GenConclAtAddr  [1]  THEN  Auto)

---

Home Index