---

{ [T:Type]
    g1,g2:LabeledGraph(T).  (g1  lg-append(g1;g2)  g2  lg-append(g1;g2)) }

{ Proof }

---

Definitions occuring in Statement :  lg-contains: g1  g2,  lg-append: lg-append(g1;g2),  labeled-graph: LabeledGraph(T),  uall: [x:A]. B[x],  all: x:A. B[x],  and: P  Q,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  and: P  Q,  lg-contains: g1  g2,  member: t  T,  exists: x:A. B[x],  prop: ,  true: True,  rev_implies: P  Q,  iff: P  Q,  squash: T,  implies: P  Q
Lemmas :  labeled-graph_wf,  lg-nil_wf,  lg-nil-append,  lg-append_wf,  squash_wf,  true_wf,  lg-append-nil

---

\mforall{}[T:Type].  \mforall{}g1,g2:LabeledGraph(T).    (g1  \msubseteq{}  lg-append(g1;g2)  \mwedge{}  g2  \msubseteq{}  lg-append(g1;g2))


Date html generated: 2011_08_16-PM-06_36_38
Last ObjectModification: 2011_06_20-AM-01_56_15

Home Index