---

Step * 1 of Lemma lg-label-map


1. f : Top
2. g : LabeledGraph(Top)
3. lg-size(g) ∈ ℕ
4. g ∈ Top List
5. g ∈ (Top × ℕlg-size(g) List × (ℕlg-size(g) List)) List
6. x : ℕlg-size(g)
⊢ lg-label(lg-map(f;g);x) ~ f lg-label(g;x)
BY
{ (GenConclAtAddr [2;2;1] THEN RepUR ``lg-label lg-map`` 0) }

1
1. f : Top
2. g : LabeledGraph(Top)
3. lg-size(g) ∈ ℕ
4. g ∈ Top List
5. g ∈ (Top × ℕlg-size(g) List × (ℕlg-size(g) List)) List
6. x : ℕlg-size(g)
7. v : (Top × ℕlg-size(g) List × (ℕlg-size(g) List)) List@i
8. g = v ∈ ((Top × ℕlg-size(g) List × (ℕlg-size(g) List)) List)@i
⊢ fst(map(λtr.let lbl,in,out = tr in 
              <f lbl, in, out>;v)[x]) ~ f (fst(v[x]))

---

Latex:

---

Latex:

1.  f  :  Top
2.  g  :  LabeledGraph(Top)
3.  lg-size(g)  \mmember{}  \mBbbN{}
4.  g  \mmember{}  Top  List
5.  g  \mmember{}  (Top  \mtimes{}  \mBbbN{}lg-size(g)  List  \mtimes{}  (\mBbbN{}lg-size(g)  List))  List
6.  x  :  \mBbbN{}lg-size(g)
\mvdash{}  lg-label(lg-map(f;g);x)  \msim{}  f  lg-label(g;x)


By

---

Latex:
(GenConclAtAddr  [2;2;1]  THEN  RepUR  ``lg-label  lg-map``  0)

---

Home Index