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