---

Step * 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)
⊢ fst(map(λtr.let lbl,in,out = tr in 
              <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2)[x - lg-size(g1)]) ~ fst(g2[x 
- lg-size(g1)])
BY
{ Assert ⌈x - lg-size(g1) < ||g2||⌉⋅ }

1
.....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||

2
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. x - lg-size(g1) < ||g2||
⊢ fst(map(λtr.let lbl,in,out = tr in 
              <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2)[x - lg-size(g1)]) ~ fst(g2[x 
- lg-size(g1)])

---

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)
\mvdash{}  fst(map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                            <lbl,  map(\mlambda{}x.(x  +  lg-size(g1));in),  map(\mlambda{}x.(x  +  lg-size(g1));out)>g2)[x 
-  lg-size(g1)])  \msim{}  fst(g2[x  -  lg-size(g1)])


By

---

Latex:
Assert  \mkleeneopen{}x  -  lg-size(g1)  <  ||g2||\mkleeneclose{}\mcdot{}

---

Home Index