---

Step * 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
⊢ ∃ga@0,gb@0:LabeledGraph(T)
   (lg-append(ga;lg-append(lg-append(g4;lg-append(g1;g5));gb)) = lg-append(ga@0;lg-append(g1;gb@0)) ∈ LabeledGraph(T))
BY
{ (InstConcl [⌈lg-append(ga;g4)⌉;⌈lg-append(g5;gb)⌉]⋅ THEN Auto) }

1
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)

---

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{}  \mexists{}ga@0,gb@0:LabeledGraph(T)
      (lg-append(ga;lg-append(lg-append(g4;lg-append(g1;g5));gb))  =  lg-append(ga@0;lg-append(g1;gb@0)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}lg-append(ga;g4)\mkleeneclose{};\mkleeneopen{}lg-append(g5;gb)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index