---

Step * 2 of Lemma lg-append-contains


1. [T] : Type
2. g1 : LabeledGraph(T)@i
3. g2 : LabeledGraph(T)@i
4. g1 ⊆ lg-append(g1;g2)
⊢ ∃ga,gb:LabeledGraph(T). (lg-append(g1;g2) = lg-append(ga;lg-append(g2;gb)) ∈ LabeledGraph(T))
BY
{ (InstConcl [⌜g1⌝;⌜lg-nil()⌝]⋅ THEN Auto THEN RWW "lg-append-nil" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  g1  :  LabeledGraph(T)@i
3.  g2  :  LabeledGraph(T)@i
4.  g1  \msubseteq{}  lg-append(g1;g2)
\mvdash{}  \mexists{}ga,gb:LabeledGraph(T).  (lg-append(g1;g2)  =  lg-append(ga;lg-append(g2;gb)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}g1\mkleeneclose{};\mkleeneopen{}lg-nil()\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  RWW  "lg-append-nil"  0  THEN  Auto)\mcdot{}

---

Home Index