{ 
[A,B,C:Type]. [P:dataflow(A;B)]. [f:B 
C].
(map-dataflow(P;b.f[b]) 
dataflow(A;C)) }
{ Proof }
Definitions occuring in Statement :
map-dataflow: map-dataflow(P;b.f[b]),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
map-dataflow: map-dataflow(P;b.f[b]),
dataflow: dataflow(A;B),
equal: s = t,
member: t T,
isect: 
x:A. B[x],
function: x:A B[x],
uall: [x:A]. B[x],
universe: Type,
so_apply: x[s],
apply: f a,
axiom: Ax,
all: x:A. B[x],
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
uimplies: b supposing a,
let: let,
so_lambda: 
x y.t[x; y],
lambda: x.A[x],
spread: spread def,
dataflow-ap: df(a),
pair: <a, b>
Lemmas :
dataflow-ap_wf,
dataflow_wf,
rec-dataflow_wf
\mforall{}[A,B,C:Type]. \mforall{}[P:dataflow(A;B)]. \mforall{}[f:B {}\mrightarrow{} C]. (map-dataflow(P;b.f[b]) \mmember{} dataflow(A;C))
Date html generated:
2011_08_10-AM-08_17_02
Last ObjectModification:
2010_12_31-PM-12_45_56
Home
Index