{ 
[A,B:Type]. (dataflow-union({}) = null-dataflow()) }
{ Proof }
Definitions occuring in Statement :
dataflow-union: dataflow-union(dfs),
null-dataflow: null-dataflow(),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
universe: Type,
equal: s = t,
empty-bag: {},
bag: bag(T)
Lemmas :
pi1_wf,
bag-combine-empty-left,
subtype_base_sq,
empty-bag_wf,
pi2_wf,
it_wf,
rec-dataflow-equal,
unit_wf,
pi1_wf_top,
top_wf,
member_wf,
dataflow-ap_wf,
bag-map_wf,
bag_wf,
dataflow_wf,
bag-combine_wf
\mforall{}[A,B:Type]. (dataflow-union(\{\}) = null-dataflow())
Date html generated:
2011_08_16-AM-09_52_50
Last ObjectModification:
2011_07_05-AM-11_15_54
Home
Index