---

Step * 1 4 of Lemma lg-size-remove


1. T : Type
2. g : LabeledGraph(T)
3. x : ℕ||g||
4. ∀[as:Top List]. ∀[n:{0...||as||}].  (||nth_tl(n;as)|| = (||as|| - n) ∈ ℤ)
⊢ (||firstn(x;g)|| + (||g|| - x + 1)) = (||g|| - 1) ∈ ℤ
BY
{ ((InstLemma `length_firstn` [⌜Top⌝]⋅ THENA Auto) THEN All (Fold `lg-size`) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

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{}  (||firstn(x;g)||  +  (||g||  -  x  +  1))  =  (||g||  -  1)


By

---

Latex:
((InstLemma  `length\_firstn`  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  (Fold  `lg-size`)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index