---

Step * 1 of Lemma lg-append-contains


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index