---

Step * 1 1 of Lemma lg-contains_transitivity


1. T : Type
2. g1 : LabeledGraph(T)@i
3. g2 : LabeledGraph(T)@i
4. g3 : LabeledGraph(T)@i
5. g4 : LabeledGraph(T)@i
6. g5 : LabeledGraph(T)@i
7. ga : LabeledGraph(T)@i
8. gb : LabeledGraph(T)@i
⊢ lg-append(ga;lg-append(lg-append(g4;lg-append(g1;g5));gb))
= lg-append(lg-append(ga;g4);lg-append(g1;lg-append(g5;gb)))
∈ LabeledGraph(T)
BY
{ (RWW "lg-append_assoc" 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g1  :  LabeledGraph(T)@i
3.  g2  :  LabeledGraph(T)@i
4.  g3  :  LabeledGraph(T)@i
5.  g4  :  LabeledGraph(T)@i
6.  g5  :  LabeledGraph(T)@i
7.  ga  :  LabeledGraph(T)@i
8.  gb  :  LabeledGraph(T)@i
\mvdash{}  lg-append(ga;lg-append(lg-append(g4;lg-append(g1;g5));gb))
=  lg-append(lg-append(ga;g4);lg-append(g1;lg-append(g5;gb)))


By

---

Latex:
(RWW  "lg-append\_assoc"  0\mcdot{}  THEN  Auto)

---

Home Index