---

Step * 1 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
9. x < ||v||
⊢ fst(map(λtr.let lbl,in,out = tr in 
              <f lbl, in, out>;v)[x]) ~ f (fst(v[x]))
BY
{ (MoveToConcl (-1)
   THEN Thin (-1)
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN (RepeatFor 2 (D -3)
         THEN Reduce 0
         THEN RepeatFor 2 ((D 0 THENA Auto))
         THEN Try (Complete (Auto))
         THEN (RWO "select-cons" 0 THENA Auto)
         THEN AutoSplit
         THEN BackThruSomeHyp
         THEN Auto)⋅) }

---

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
9.  x  <  ||v||
\mvdash{}  fst(map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                            <f  lbl,  in,  out>v)[x])  \msim{}  f  (fst(v[x]))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  (RepeatFor  2  (D  -3)
              THEN  Reduce  0
              THEN  RepeatFor  2  ((D  0  THENA  Auto))
              THEN  Try  (Complete  (Auto))
              THEN  (RWO  "select-cons"  0  THENA  Auto)
              THEN  AutoSplit
              THEN  BackThruSomeHyp
              THEN  Auto)\mcdot{})

---

Home Index