---

Step * 1 3 of Lemma lg-nil-append


1. T : Type
2. g : LabeledGraph(T)
3. G : (T × ℤ List × (ℤ List)) List@i
4. g = G ∈ ((T × ℤ List × (ℤ List)) List)@i
⊢ map(λtr.let lbl,in,out = tr in 
          <lbl, map(λx.(x + 0);in), map(λx.(x + 0);out)>;G) ~ G
BY
{ (All Thin THEN ListInd (-1) THEN Reduce 0) }

1
1. T : Type
⊢ [] ~ []

2
1. T : Type
2. u : T × ℤ List × (ℤ List)
3. v : (T × ℤ List × (ℤ List)) List
4. map(λtr.let lbl,in,out = tr in 
           <lbl, map(λx.(x + 0);in), map(λx.(x + 0);out)>;v) ~ v
⊢ [let lbl,in,out = u in 
   <lbl, map(λx.(x + 0);in), map(λx.(x + 0);out)> / 
   map(λtr.let lbl,in,out = tr in 
           <lbl, map(λx.(x + 0);in), map(λx.(x + 0);out)>;v)] ~ [u / v]

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  G  :  (T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List@i
4.  g  =  G@i
\mvdash{}  map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                    <lbl,  map(\mlambda{}x.(x  +  0);in),  map(\mlambda{}x.(x  +  0);out)>G)  \msim{}  G


By

---

Latex:
(All  Thin  THEN  ListInd  (-1)  THEN  Reduce  0)

---

Home Index