---

Step * 1 of Lemma lg-size-remove


1. T : Type
2. g : LabeledGraph(T)
3. x : ℕlg-size(g)
⊢ (||firstn(x;g)|| + ||nth_tl(x + 1;g)||) = (||g|| - 1) ∈ ℤ
BY
{ (Unfold `lg-size` -1
   THEN (InstLemma `length_nth_tl` [⌈Top⌉]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto
   THEN Try ((Fold `lg-size` 0 THEN Complete (Auto)))) }

1
.....wf..... 
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)|| ∈ ℤ

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

3
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) ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  x  :  \mBbbN{}lg-size(g)
\mvdash{}  (||firstn(x;g)||  +  ||nth\_tl(x  +  1;g)||)  =  (||g||  -  1)


By

---

Latex:
(Unfold  `lg-size`  -1
  THEN  (InstLemma  `length\_nth\_tl`  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  Try  ((Fold  `lg-size`  0  THEN  Complete  (Auto))))

---

Home Index