---

Step * of Lemma lg-contains_transitivity

∀[T:Type]. ∀g1,g2,g3:LabeledGraph(T).  (g1 ⊆ g2 ⇒ g2 ⊆ g3 ⇒ g1 ⊆ g3)
BY
{ (Unfold `lg-contains` 0
   THEN Auto
   THEN ExRepD
   THEN (HypSubst' (-1) 0 THEN Auto THEN Thin (-1))
   THEN HypSubst' (-3) 0
   THEN Auto
   THEN Thin (-3)) }

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
⊢ ∃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))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}g1,g2,g3:LabeledGraph(T).    (g1  \msubseteq{}  g2  {}\mRightarrow{}  g2  \msubseteq{}  g3  {}\mRightarrow{}  g1  \msubseteq{}  g3)


By

---

Latex:
(Unfold  `lg-contains`  0
  THEN  Auto
  THEN  ExRepD
  THEN  (HypSubst'  (-1)  0  THEN  Auto  THEN  Thin  (-1))
  THEN  HypSubst'  (-3)  0
  THEN  Auto
  THEN  Thin  (-3))

---

Home Index