---

Step * 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))
⊢ fst(g1 @ 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]) ~ i\000Cf x <z lg-size(g1)
then fst(g1[x])
else fst(g2[x - lg-size(g1)])
fi 
BY
{ ((RWO "select-append" 0 THENM Fold `lg-size` 0 THENM AutoSplit) THENA 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)
⊢ 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))
\mvdash{}  fst(g1
@  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]) 
\msim{}  if  x  <z  lg-size(g1)  then  fst(g1[x])  else  fst(g2[x  -  lg-size(g1)])  fi 


By

---

Latex:
((RWO  "select-append"  0  THENM  Fold  `lg-size`  0  THENM  AutoSplit)  THENA  Auto)

---

Home Index