{ 
[A,B,S,C:Type]. [s0:S]. [G:S 
A (S 
B)]. [f:B C].
(map-dataflow(rec-dataflow(s0;s,a.G[s;a]);x.f[x])
= rec-dataflow(s0;s,a.let s',b = G[s;a]
in <s', f[b]>)) }
{ Proof }
Definitions occuring in Statement :
map-dataflow: map-dataflow(P;b.f[b]),
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
function: x:A B[x],
spread: spread def,
pair: <a, b>,
product: x:A B[x],
universe: Type,
equal: s = t
Definitions :
sqequal: s ~ t,
subtype: S 
T,
prop: 
,
true: True,
squash: 
T,
data-stream: data-stream(P;L),
list: type List,
let: let,
lambda: 
x.A[x],
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
all: x:A. B[x],
axiom: Ax,
pair: <a, b>,
spread: spread def,
so_apply: x[s],
apply: f a,
so_apply: x[s1;s2],
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
map-dataflow: map-dataflow(P;b.f[b]),
dataflow: dataflow(A;B),
equal: s = t,
universe: Type,
uall: [x:A]. B[x],
product: x:A B[x],
function: x:A B[x],
isect: 
x:A. B[x],
member: t 
T,
Auto: Error :Auto,
THENM: Error :THENM,
CollapseTHENA: Error :CollapseTHENA,
Complete: Error :Complete,
CollapseTHEN: Error :CollapseTHEN,
Try: Error :Try,
tactic: Error :tactic,
tl: tl(l),
hd: hd(l),
cons: [car / cdr],
map: map(f;as),
data_stream_nil: data_stream_nil{data_stream_nil_compseq_tag_def:o}(P),
nil: [],
implies: P 
Q,
pi2: snd(t),
dataflow-ap: df(a),
pi1: fst(t),
rec_dataflow_ap: rec_dataflow_ap_compseq_tag_def,
void: Void,
top: Top
Lemmas :
data-stream-cons,
top_wf,
dataflow-extensionality,
map-dataflow_wf,
rec-dataflow_wf,
data-stream_wf,
squash_wf,
true_wf,
member_wf,
dataflow_wf,
map-data-stream
\mforall{}[A,B,S,C:Type]. \mforall{}[s0:S]. \mforall{}[G:S {}\mrightarrow{} A {}\mrightarrow{} (S \mtimes{} B)]. \mforall{}[f:B {}\mrightarrow{} C].
(map-dataflow(rec-dataflow(s0;s,a.G[s;a]);x.f[x])
= rec-dataflow(s0;s,a.let s',b = G[s;a]
in <s', f[b]>))
Date html generated:
2011_08_10-AM-08_20_17
Last ObjectModification:
2011_06_18-AM-08_32_03
Home
Index