{ 
[T:Type]. [a,b,c:LabeledGraph(T)].
(lg-append(a;lg-append(b;c)) ~ lg-append(lg-append(a;b);c)) }
{ Proof }
Definitions occuring in Statement :
lg-append: lg-append(g1;g2),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
universe: Type,
sqequal: s ~ t
Definitions :
lg-append: lg-append(g1;g2),
member: t 
T,
top: Top,
compose: f o g,
all: x:A. B[x],
implies: P 
Q,
map: map(f;as),
spreadn: spread3,
lg-size: lg-size(g),
ycomb: Y,
labeled-graph: LabeledGraph(T),
int_seg: {i..j
},
uall: [x:A]. B[x],
uimplies: b supposing a,
sq_type: SQType(T),
nat: 
,
guard: {T}
Lemmas :
top_wf,
length_wf1,
subtype_rel_list,
int_seg_wf,
subtype_rel_simple_product,
subtype_rel_self,
int_seg_properties,
labeled-graph_wf,
map_append_sq,
map-map,
append_assoc_sq,
length-append,
map_wf,
length-map-sq,
subtype_base_sq,
int_subtype_base,
length_wf_nat,
nat_wf
\mforall{}[T:Type]. \mforall{}[a,b,c:LabeledGraph(T)]. (lg-append(a;lg-append(b;c)) \msim{} lg-append(lg-append(a;b);c))
Date html generated:
2011_08_16-PM-06_36_05
Last ObjectModification:
2011_06_20-AM-01_55_29
Home
Index