{ 
[S,A,B:Type]. [s0:S]. [next:S 
A (S 
B)]. [L:A List].
(rec-dataflow-state(s0;s,m.next[s;m];L) 
S) }
{ Proof }
Definitions occuring in Statement :
rec-dataflow-state: rec-dataflow-state(s0;s,m.next[s; m];L),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type
Definitions :
isect: 
x:A. B[x],
list: type List,
member: t T,
uall: [x:A]. B[x],
function: x:A B[x],
product: x:A B[x],
universe: Type,
equal: s = t,
rec-dataflow-state: rec-dataflow-state(s0;s,m.next[s; m];L),
so_apply: x[s1;s2],
apply: f a,
axiom: Ax,
list_accum: list_accum(x,a.f[x; a];y;l),
all: x:A. B[x],
so_lambda: 
x y.t[x; y],
lambda: x.A[x],
pi1: fst(t),
top: Top,
subtype: S 
T,
void: Void
Lemmas :
member_wf,
top_wf,
pi1_wf_top,
list_accum_wf
\mforall{}[S,A,B:Type]. \mforall{}[s0:S]. \mforall{}[next:S {}\mrightarrow{} A {}\mrightarrow{} (S \mtimes{} B)]. \mforall{}[L:A List].
(rec-dataflow-state(s0;s,m.next[s;m];L) \mmember{} S)
Date html generated:
2011_08_10-AM-08_14_06
Last ObjectModification:
2011_06_16-PM-04_45_47
Home
Index