---

Step * 1 of Lemma lg-all-append


1. [T] : Type
2. [P] : T ─→ ℙ
3. g1 : LabeledGraph(T)
4. lg-size(g1) ∈ ℕ
5. g1 ∈ Top List
6. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
7. g2 : LabeledGraph(T)
8. lg-size(g2) ∈ ℕ
9. g2 ∈ Top List
10. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
11. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
⊢ ∀n:ℕlg-size(lg-append(g1;g2)). P[lg-label(lg-append(g1;g2);n)]
⇐⇒ (∀n:ℕlg-size(g1). P[lg-label(g1;n)]) ∧ (∀n:ℕlg-size(g2). P[lg-label(g2;n)])
BY
{ ((RepeatFor 2 (D 0)
    THENA RepeatFor 3 ((MemCD THEN Try (Complete (Auto)) THEN Try ((BLemma `lg-label_wf` THEN Auto))))
    )
   THEN Auto
   ) }

1
1. [T] : Type
2. [P] : T ─→ ℙ
3. g1 : LabeledGraph(T)
4. lg-size(g1) ∈ ℕ
5. g1 ∈ Top List
6. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
7. g2 : LabeledGraph(T)
8. lg-size(g2) ∈ ℕ
9. g2 ∈ Top List
10. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
11. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
12. ∀n:ℕlg-size(lg-append(g1;g2)). P[lg-label(lg-append(g1;g2);n)]@i
13. n : ℕlg-size(g1)@i
⊢ P[lg-label(g1;n)]

2
1. [T] : Type
2. [P] : T ─→ ℙ
3. g1 : LabeledGraph(T)
4. lg-size(g1) ∈ ℕ
5. g1 ∈ Top List
6. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
7. g2 : LabeledGraph(T)
8. lg-size(g2) ∈ ℕ
9. g2 ∈ Top List
10. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
11. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
12. ∀n:ℕlg-size(lg-append(g1;g2)). P[lg-label(lg-append(g1;g2);n)]@i
13. ∀n:ℕlg-size(g1). P[lg-label(g1;n)]
14. n : ℕlg-size(g2)@i
⊢ P[lg-label(g2;n)]

3
1. [T] : Type
2. [P] : T ─→ ℙ
3. g1 : LabeledGraph(T)
4. lg-size(g1) ∈ ℕ
5. g1 ∈ Top List
6. g1 ∈ (T × ℕlg-size(g1) List × (ℕlg-size(g1) List)) List
7. g2 : LabeledGraph(T)
8. lg-size(g2) ∈ ℕ
9. g2 ∈ Top List
10. g2 ∈ (T × ℕlg-size(g2) List × (ℕlg-size(g2) List)) List
11. lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ
12. ∀n:ℕlg-size(g1). P[lg-label(g1;n)]@i
13. ∀n:ℕlg-size(g2). P[lg-label(g2;n)]@i
14. n : ℕlg-size(lg-append(g1;g2))@i
⊢ P[lg-label(lg-append(g1;g2);n)]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  g1  :  LabeledGraph(T)
4.  lg-size(g1)  \mmember{}  \mBbbN{}
5.  g1  \mmember{}  Top  List
6.  g1  \mmember{}  (T  \mtimes{}  \mBbbN{}lg-size(g1)  List  \mtimes{}  (\mBbbN{}lg-size(g1)  List))  List
7.  g2  :  LabeledGraph(T)
8.  lg-size(g2)  \mmember{}  \mBbbN{}
9.  g2  \mmember{}  Top  List
10.  g2  \mmember{}  (T  \mtimes{}  \mBbbN{}lg-size(g2)  List  \mtimes{}  (\mBbbN{}lg-size(g2)  List))  List
11.  lg-size(lg-append(g1;g2))  =  (lg-size(g1)  +  lg-size(g2))
\mvdash{}  \mforall{}n:\mBbbN{}lg-size(lg-append(g1;g2)).  P[lg-label(lg-append(g1;g2);n)]
\mLeftarrow{}{}\mRightarrow{}  (\mforall{}n:\mBbbN{}lg-size(g1).  P[lg-label(g1;n)])  \mwedge{}  (\mforall{}n:\mBbbN{}lg-size(g2).  P[lg-label(g2;n)])


By

---

Latex:
((RepeatFor  2  (D  0)
    THENA  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))  THEN  Try  ((BLemma  `lg-label\_wf`  THEN  Auto))))
    )
  THEN  Auto
  )

---

Home Index