{ 
[T:Type]. [S:Id List]. [F:information-flow(T;S)]. [G:Graph(S)].
(flow-graph(S;T;F;G) 
) }
{ Proof }
Definitions occuring in Statement :
flow-graph: flow-graph(S;T;F;G),
information-flow: information-flow(T;S),
id-graph: Graph(S),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
information-flow: information-flow(T;S),
member: t T,
prop: ,
flow-graph: flow-graph(S;T;F;G),
all: x:A. B[x],
implies: P 
Q,
top: Top,
subtype: S 
T,
suptype: suptype(S; T)
Lemmas :
Id_wf,
l_member_wf,
length_wf1,
assert_wf,
can-apply_wf,
top_wf,
id-graph-edge_wf,
id-graph_wf,
information-flow_wf
\mforall{}[T:Type]. \mforall{}[S:Id List]. \mforall{}[F:information-flow(T;S)]. \mforall{}[G:Graph(S)]. (flow-graph(S;T;F;G) \mmember{} \mBbbP{})
Date html generated:
2011_08_16-AM-11_02_10
Last ObjectModification:
2011_06_18-AM-09_35_37
Home
Index