{ 
[A:
']. [B:Type]. (null-dataflow() 
dataflow(A;bag(B))) }
{ Proof }
Definitions occuring in Statement :
null-dataflow: null-dataflow(),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
empty-bag: Error :empty-bag,
pair: <a, b>,
lambda: 
x.A[x],
unit: Unit,
it: 
,
so_lambda: 
x y.t[x; y],
apply: f a,
let: let,
uimplies: b supposing a,
function: x:A 
B[x],
all: x:A. B[x],
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
dataflow: dataflow(A;B),
bag: Error :bag,
null-dataflow: null-dataflow(),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
equal: s = t,
member: t T,
universe: Type
Lemmas :
rec-dataflow_wf,
Error :bag_wf,
it_wf,
Error :empty-bag_wf,
unit_wf
\mforall{}[A:\mBbbU{}']. \mforall{}[B:Type]. (null-dataflow() \mmember{} dataflow(A;bag(B)))
Date html generated:
2011_08_10-AM-08_17_58
Last ObjectModification:
2011_02_03-PM-01_01_03
Home
Index