{ 
[T:Type]. Assoc(LabeledGraph(T);
a,b.lg-append(a;b)) }
{ Proof }
Definitions occuring in Statement :
lg-append: lg-append(g1;g2),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
lambda: x.A[x],
universe: Type,
assoc: Assoc(T;op)
Definitions :
uall: [x:A]. B[x],
assoc: Assoc(T;op),
member: t 
T,
infix_ap: x f y
Lemmas :
lg-append_assoc,
lg-append_wf,
labeled-graph_wf
\mforall{}[T:Type]. Assoc(LabeledGraph(T);\mlambda{}a,b.lg-append(a;b))
Date html generated:
2011_08_16-PM-06_36_11
Last ObjectModification:
2011_06_20-AM-01_55_38
Home
Index