{ 
[T,S:Type]. [f:T 
S]. [g:LabeledGraph(T)].
(lg-map(f;g) 
LabeledGraph(S)) }
{ Proof }
Definitions occuring in Statement :
lg-map: lg-map(f;g),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
labeled-graph: LabeledGraph(T),
member: t T,
lg-map: lg-map(f;g),
top: Top,
spreadn: spread3,
all: x:A. B[x],
implies: P 
Q,
so_lambda: 
x.t[x],
nat: 
,
so_apply: x[s],
lg-size: lg-size(g),
guard: {T}
Lemmas :
map-is-top-list,
length-map-sq,
lg-size_wf,
map_wf,
int_seg_wf,
nat_wf,
nat_properties,
Error :dep-isect_wf,
top_wf,
length_wf1
\mforall{}[T,S:Type]. \mforall{}[f:T {}\mrightarrow{} S]. \mforall{}[g:LabeledGraph(T)]. (lg-map(f;g) \mmember{} LabeledGraph(S))
Date html generated:
2011_08_16-PM-06_44_15
Last ObjectModification:
2011_06_18-AM-10_56_04
Home
Index