{ 
[A,B:Type]. [d:dataflow(A;bag(B))]. (dataflow-union({d}) = d) }
{ Proof }
Definitions occuring in Statement :
dataflow-union: dataflow-union(dfs),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
universe: Type,
equal: s = t,
single-bag: {x},
bag: bag(T)
Lemmas :
member_wf,
top_wf,
pi1_wf_top,
isect_subtype_base,
nat_wf,
primrec_wf,
product_subtype_base,
subtype_base_sq,
bag-combine-single-left,
pi1_wf,
dataflow-equal,
single-bag_wf,
dataflow-union_wf,
iterate-dataflow_wf,
dataflow-ap_wf,
dataflow_wf,
pi2_wf,
bag_wf
\mforall{}[A,B:Type]. \mforall{}[d:dataflow(A;bag(B))]. (dataflow-union(\{d\}) = d)
Date html generated:
2011_08_16-AM-09_52_53
Last ObjectModification:
2011_07_05-AM-11_18_22
Home
Index