---

Step * of Lemma lg-append_wf

∀[T:Type]. ∀[g1,g2:LabeledGraph(T)].  (lg-append(g1;g2) ∈ LabeledGraph(T))
BY
{ (ProveWfLemma THEN All (Unfold `labeled-graph`)) }

1
1. T : Type
2. g1 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g2 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
⊢ g1 @ map(λtr.let lbl,in,out = tr in <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2) ∈ self:Top \000CList ∩ (T
                                                                                        × ℕ||self|| List
                                                                                        × (ℕ||self|| List)) List

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g1,g2:LabeledGraph(T)].    (lg-append(g1;g2)  \mmember{}  LabeledGraph(T))


By

---

Latex:
(ProveWfLemma  THEN  All  (Unfold  `labeled-graph`))

---

Home Index