{ 
[S,A,B:Type]. [s0:S]. [next:S 
A (S 
B)].
(rec-dataflow(s0;s,m.next[s;m]) 
dataflow(A;B)) }
{ Proof }
Definitions occuring in Statement :
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
so_apply: x[s1;s2],
member: t T,
function: x:A B[x],
product: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
dataflow: dataflow(A;B),
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
so_apply: x[s1;s2],
corec: corec(T.F[T]),
ycomb: Y,
primrec: primrec(n;b;c),
top: Top,
all: x:A. B[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =
j),
btrue: tt,
bfalse: ff,
implies: P 
Q,
prop: 
,
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
bool: 
,
unit: Unit,
iff: P 
Q,
and: P 
Q,
nat: 
,
it: 
,
guard: {T}
Lemmas :
nat_wf,
ycomb-unroll,
eq_int_wf,
bool_wf,
iff_weakening_uiff,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_eq_int,
not_wf,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
nat_properties,
ge_wf
\mforall{}[S,A,B:Type]. \mforall{}[s0:S]. \mforall{}[next:S {}\mrightarrow{} A {}\mrightarrow{} (S \mtimes{} B)]. (rec-dataflow(s0;s,m.next[s;m]) \mmember{} dataflow(A;B))
Date html generated:
2011_08_10-AM-08_13_56
Last ObjectModification:
2011_06_18-AM-08_29_38
Home
Index