---

Step * 1 3 1 of Lemma lg-size-remove


1. T : Type
2. g : LabeledGraph(T)
3. x : ℕlg-size(g)
⊢ x + 1 ∈ {0...lg-size(g)}
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  x  :  \mBbbN{}lg-size(g)
\mvdash{}  x  +  1  \mmember{}  \{0...lg-size(g)\}


By

---

Latex:
Auto

---

Home Index