---

Step * 1 of Lemma lg-nil-append


1. T : Type
2. g : LabeledGraph(T)
⊢ map(λtr.let lbl,in,out = tr in 
          <lbl, map(λx.(x + 0);in), map(λx.(x + 0);out)>;g) ~ g
BY
{ GenConcl ⌈g = G ∈ ((T × ℤ List × (ℤ List)) List)⌉⋅ }

1
.....wf..... 
1. T : Type
2. g : LabeledGraph(T)
⊢ g ∈ (T × ℤ List × (ℤ List)) List

2
.....wf..... 
1. T : Type
2. g : LabeledGraph(T)
⊢ (T × ℤ List × (ℤ List)) List ∈ Type

3
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

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
\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:
GenConcl  \mkleeneopen{}g  =  G\mkleeneclose{}\mcdot{}

---

Home Index