{ 
[A,B,C:Type]. [P,Q:dataflow(A;B)]. [f:B 
C].
map-dataflow(P;x.f[x]) 
map-dataflow(Q;x.f[x]) supposing P Q }
{ Proof }
Definitions occuring in Statement :
dataflow-equiv: d1 d2,
map-dataflow: map-dataflow(P;b.f[b]),
dataflow: dataflow(A;B),
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
function: x:A B[x],
universe: Type
Definitions :
tactic: Error :tactic,
RepeatFor: Error :RepeatFor,
ParallelOp: Error :ParallelOp,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
set: {x:A| B[x]} ,
combination: Combination(n;T),
listp: A List
,
isect: 
x:A. B[x],
member: t 
T,
function: x:A B[x],
uall: [x:A]. B[x],
dataflow: dataflow(A;B),
universe: Type,
equal: s = t,
all: x:A. B[x],
dataflow-equiv: d1 d2,
uimplies: b supposing a,
prop: 
,
lambda: 
x.A[x],
list: type List,
data-stream: data-stream(P;L),
map-dataflow: map-dataflow(P;b.f[b]),
so_apply: x[s],
apply: f a,
axiom: Ax,
subtype_rel: A 
r B,
uiff: uiff(P;Q),
and: P 
Q,
product: x:A 
B[x],
less_than: a < b,
not: 
A,
ge: i 
j ,
le: A 
B,
corec: corec(T.F[T]),
strong-subtype: strong-subtype(A;B),
so_lambda: 
x.t[x],
sqequal: s ~ t,
map: map(f;as)
Lemmas :
map-data-stream,
dataflow_wf,
dataflow-equiv_wf,
map_wf
\mforall{}[A,B,C:Type]. \mforall{}[P,Q:dataflow(A;B)]. \mforall{}[f:B {}\mrightarrow{} C].
map-dataflow(P;x.f[x]) \mequiv{} map-dataflow(Q;x.f[x]) supposing P \mequiv{} Q
Date html generated:
2011_08_10-AM-08_23_07
Last ObjectModification:
2011_06_18-AM-08_32_49
Home
Index