---

Step * of Lemma lg-size-remove

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)].  (lg-size(lg-remove(g;x)) = (lg-size(g) - 1) ∈ ℤ)
BY
{ (Auto THEN RepUR ``lg-size lg-remove`` 0 THEN (RWW "length-map-sq length-append length_firstn" 0 THENA Auto)) }

1
1. T : Type
2. g : LabeledGraph(T)
3. x : ℕlg-size(g)
⊢ (||firstn(x;g)|| + ||nth_tl(x + 1;g)||) = (||g|| - 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].  \mforall{}[x:\mBbbN{}lg-size(g)].    (lg-size(lg-remove(g;x))  =  (lg-size(g)  -  1))


By

---

Latex:
(Auto
  THEN  RepUR  ``lg-size  lg-remove``  0
  THEN  (RWW  "length-map-sq  length-append  length\_firstn"  0  THENA  Auto))

---

Home Index