{ 
[A,C:Type]. [n:
]. [B:n 
Type]. [ds:k:n dataflow(A;B[k])].
[F:k:n B[k] C C]. [s:C]. [P:C 
].
(feedback-dataflow(ds;
F;s;x.P[x]) 
dataflow(A;C)) }
{ Proof }
Definitions occuring in Statement :
feedback-dataflow: feedback-dataflow,
dataflow: dataflow(A;B),
bool: ,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
natural_number: $n,
universe: Type
Definitions :
axiom: Ax,
feedback-dataflow: feedback-dataflow,
bool: ,
apply: f a,
so_apply: x[s],
dataflow: dataflow(A;B),
set: {x:A| B[x]} ,
real: 
,
grp_car: |g|,
subtype: S 
T,
all: x:A. B[x],
int: 
,
natural_number: $n,
nat: ,
equal: s = t,
function: x:A B[x],
universe: Type,
int_seg: {i..j},
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t T,
Repeat: Error :Repeat,
CollapseTHEN: Error :CollapseTHEN,
void: Void,
top: Top,
corec: corec(T.F[T]),
strong-subtype: strong-subtype(A;B),
list: type List,
less_than: a < b,
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
fpf: a:A fp-> B[a],
guard: {T},
sq_type: SQType(T),
implies: P 
Q,
false: False,
not: 
A,
dataflow-out: dataflow-out(df;a),
ifthenelse: if b then t else f fi ,
dataflow-ap: df(a),
pi1: fst(t),
spread: spread def,
lambda: 
x.A[x],
product: x:A 
B[x],
pair: <a, b>,
so_lambda: 
x y.t[x; y],
let: let,
uimplies: b supposing a,
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
le: A 
B,
ge: i 
j
Lemmas :
member_wf,
nat_properties,
rec-dataflow_wf,
dataflow-out_wf,
pi1_wf_top,
dataflow-ap_wf,
top_wf,
ifthenelse_wf,
nat_wf,
dataflow_wf,
int_seg_wf,
bool_wf
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C {}\mrightarrow{} C].
\mforall{}[s:C]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}].
(feedback-dataflow(ds;
F;s;x.P[x]) \mmember{} dataflow(A;C))
Date html generated:
2011_08_10-AM-08_18_30
Last ObjectModification:
2011_06_18-AM-08_31_39
Home
Index