---

Step * 1 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)
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]))
BY
{ (Assert x < ||v|| BY
         ((RevHypSubst' (-1) 0 THENA Auto) THEN Fold `lg-size` 0 THEN Auto)) }

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
9. x < ||v||
⊢ 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)
7.  v  :  (Top  \mtimes{}  \mBbbN{}lg-size(g)  List  \mtimes{}  (\mBbbN{}lg-size(g)  List))  List@i
8.  g  =  v@i
\mvdash{}  fst(map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                            <f  lbl,  in,  out>v)[x])  \msim{}  f  (fst(v[x]))


By

---

Latex:
(Assert  x  <  ||v||  BY
              ((RevHypSubst'  (-1)  0  THENA  Auto)  THEN  Fold  `lg-size`  0  THEN  Auto))

---

Home Index