---

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


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)
BY
{ Auto' }

---

Latex:

---

Latex:

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)
12.  lg-size(lg-append(g1;g2))  =  (lg-size(g1)  +  lg-size(g2))
\mvdash{}  x  -  lg-size(g1)  <  lg-size(g2)


By

---

Latex:
Auto'

---

Home Index