---

Step * 1 1 1 2 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. x - lg-size(g1) < ||g2||
⊢ fst(((λ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\000C)])) ~ fst(g2[x 
- lg-size(g1)])
BY
{ ((GenConclAtAddr [2;1] THEN Try (Complete (Auto'))) THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN 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.  x  -  lg-size(g1)  <  ||g2||
\mvdash{}  fst(((\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:
((GenConclAtAddr  [2;1]  THEN  Try  (Complete  (Auto')))  THEN  RepeatFor  2  (D  -2)  THEN  Reduce  0  THEN  Auto)

---

Home Index