{ 
[A,B:Type]. [f,g:dataflow(A;B)]. f 
g supposing f = g }
{ Proof }
Definitions occuring in Statement :
dataflow-equiv: d1 d2,
dataflow: dataflow(A;B),
uimplies: b supposing a,
uall: [x:A]. B[x],
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
dataflow-equiv: d1 d2,
member: t 
T,
prop: 
,
all: x:A. B[x]
Lemmas :
dataflow-equiv_wf,
dataflow_wf,
data-stream_wf
\mforall{}[A,B:Type]. \mforall{}[f,g:dataflow(A;B)]. f \mequiv{} g supposing f = g
Date html generated:
2011_08_10-AM-08_21_46
Last ObjectModification:
2011_06_18-AM-08_32_27
Home
Index