---

Step * 1 3 of Lemma lg-size-remove

.....wf..... 
1. T : Type
2. g : LabeledGraph(T)
3. x : ℕ||g||
4. ∀[as:Top List]. ∀[n:{0...||as||}].  (||nth_tl(n;as)|| = (||as|| - n) ∈ ℤ)
⊢ x + 1 ∈ {0...||g||}
BY
{ (Thin (-1) THEN Fold `lg-size` 0 THEN Fold `lg-size` (-1)) }

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

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  x  :  \mBbbN{}||g||
4.  \mforall{}[as:Top  List].  \mforall{}[n:\{0...||as||\}].    (||nth\_tl(n;as)||  =  (||as||  -  n))
\mvdash{}  x  +  1  \mmember{}  \{0...||g||\}


By

---

Latex:
(Thin  (-1)  THEN  Fold  `lg-size`  0  THEN  Fold  `lg-size`  (-1))

---

Home Index