{ 
[T:Type]. [g1,g2:LabeledGraph(T)]. (lg-append(g1;g2) 
LabeledGraph(T)) }
{ Proof }
Definitions occuring in Statement :
lg-append: lg-append(g1;g2),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
labeled-graph: LabeledGraph(T),
member: t T,
lg-append: lg-append(g1;g2),
all: x:A. B[x],
implies: P 
Q,
top: Top,
nat: 
,
so_lambda: 
x.t[x],
int_seg: {i..j
},
lelt: i 
j < k,
and: P 
Q,
le: A B,
not: 
A,
false: False,
spreadn: spread3,
lg-size: lg-size(g),
sq_type: SQType(T),
uimplies: b supposing a,
so_apply: x[s],
guard: {T},
prop: 
Lemmas :
labeled-graph_wf,
top_wf,
length_wf1,
append_wf,
map_wf,
int_seg_wf,
subtype_base_sq,
nat_wf,
set_subtype_base,
le_wf,
int_subtype_base,
length-append,
length-map,
non_neg_length,
length_wf_nat,
subtype_rel_list,
subtype_rel_simple_product,
subtype_rel_self,
int_seg_properties
\mforall{}[T:Type]. \mforall{}[g1,g2:LabeledGraph(T)]. (lg-append(g1;g2) \mmember{} LabeledGraph(T))
Date html generated:
2011_08_16-PM-06_35_58
Last ObjectModification:
2011_06_20-AM-01_55_19
Home
Index