---

Step * 1 1 1 1 of Lemma lg-label-append

.....assertion..... 
1. T : Type
2. g1 : LabeledGraph(T)
3. lg-size(g1) ∈ ℕ
4. g1 ∈ Top List
5. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
6. g2 : LabeledGraph(T)
7. lg-size(g2) ∈ ℕ
8. g2 ∈ Top List
9. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
10. x : ℕlg-size(lg-append(g1;g2))
11. ¬x < lg-size(g1)
⊢ x - lg-size(g1) < ||g2||
BY
{ (Fold `lg-size` 0
   THEN (Assert lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ BY
               (RepUR ``lg-size lg-append`` 0
                THEN RWW "length-append length-map-sq" 0
                THEN Try (Fold `lg-size` 0)
                THEN Auto))
   ) }

1
1. T : Type
2. g1 : LabeledGraph(T)
3. lg-size(g1) ∈ ℕ
4. g1 ∈ Top List
5. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
6. g2 : LabeledGraph(T)
7. lg-size(g2) ∈ ℕ
8. g2 ∈ Top List
9. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
10. x : ℕlg-size(lg-append(g1;g2))
11. ¬x < lg-size(g1)
12. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
⊢ x - lg-size(g1) < lg-size(g2)

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  g1  :  LabeledGraph(T)
3.  lg-size(g1)  \mmember{}  \mBbbN{}
4.  g1  \mmember{}  Top  List
5.  g1  \mmember{}  (T  \mtimes{}  \mBbbN{}lg-size(g1)  List  \mtimes{}  (\mBbbN{}lg-size(g1)  List))  List
6.  g2  :  LabeledGraph(T)
7.  lg-size(g2)  \mmember{}  \mBbbN{}
8.  g2  \mmember{}  Top  List
9.  g2  \mmember{}  (T  \mtimes{}  \mBbbN{}lg-size(g2)  List  \mtimes{}  (\mBbbN{}lg-size(g2)  List))  List
10.  x  :  \mBbbN{}lg-size(lg-append(g1;g2))
11.  \mneg{}x  <  lg-size(g1)
\mvdash{}  x  -  lg-size(g1)  <  ||g2||


By

---

Latex:
(Fold  `lg-size`  0
  THEN  (Assert  lg-size(lg-append(g1;g2))  =  (lg-size(g1)  +  lg-size(g2))  BY
                          (RepUR  ``lg-size  lg-append``  0
                            THEN  RWW  "length-append  length-map-sq"  0
                            THEN  Try  (Fold  `lg-size`  0)
                            THEN  Auto))
  )

---

Home Index