{ 
[S,A,B:Type]. [next:S 
A (S 
B)]. [L:A List]. [s0:S].
(rec-dataflow(s0;s,m.next[s;m])*(L)
~ rec-dataflow(rec-dataflow-state(s0;s,m.next[s;m];L);s,m.next[s;m])) }
{ Proof }
Definitions occuring in Statement :
iterate-dataflow: P*(inputs),
rec-dataflow-state: rec-dataflow-state(s0;s,m.next[s; m];L),
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type,
sqequal: s ~ t
Definitions :
tactic: Error :tactic,
Unfold: Error :Unfold,
Auto: Error :Auto,
D: Error :D,
CollapseTHEN: Error :CollapseTHEN,
BHyp: Error :BHyp,
universe: Type,
product: x:A B[x],
function: x:A B[x],
list: type List,
prop: 
,
sqequal: s ~ t,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
isect: 
x:A. B[x],
rec-dataflow-state: rec-dataflow-state(s0;s,m.next[s; m];L),
member: t 
T,
equal: s = t,
iter_df_nil: iter_df_nil{iter_df_nil_compseq_tag_def:o}(P),
iter_df_cons: iter_df_cons{iter_df_cons_compseq_tag_def:o}(as; a; P),
rec_dataflow_ap: rec_dataflow_ap_compseq_tag_def,
iterate-dataflow: P*(inputs),
pi1: fst(t),
spread: spread def,
so_apply: x[s1;s2],
apply: f a,
pair: <a, b>,
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
list_accum: list_accum(x,a.f[x; a];y;l),
all: x:A. B[x],
subtype_rel: A 
r B,
so_lambda: x y.t[x; y],
uiff: uiff(P;Q),
and: P 
Q,
uimplies: b supposing a,
less_than: a < b,
not: 
A,
ge: i 
j ,
le: A 
B,
strong-subtype: strong-subtype(A;B),
implies: P 
Q
Lemmas :
uall_wf
\mforall{}[S,A,B:Type]. \mforall{}[next:S {}\mrightarrow{} A {}\mrightarrow{} (S \mtimes{} B)]. \mforall{}[L:A List]. \mforall{}[s0:S].
(rec-dataflow(s0;s,m.next[s;m])*(L) \msim{} rec-dataflow(rec-dataflow-state(s0;s,m.next[s;m];L);
s,m.next[s;m]))
Date html generated:
2011_08_10-AM-08_14_26
Last ObjectModification:
2011_06_16-PM-04_55_05
Home
Index