Nuprl Lemma : better-feedback-dataflow_functionality
[A,C:Type]. [n:
]. [B:n 
Type]. [F:k:n B[k] C C]. [ds1,ds2:k:n dataflow(A;B[k])]. [buf:C].
[P:C 
].
better-feedback-dataflow(n;ds1;F;buf;x.P[x]) 
better-feedback-dataflow(n;ds2;F;buf;x.P[x])
supposing k:n. ds1 k ds2 k
Proof not projected
Definitions occuring in Statement :
dataflow-equiv: d1 d2,
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
dataflow: dataflow(A;B),
bool: ,
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
apply: f a,
function: x:A B[x],
natural_number: $n,
universe: Type
Definitions :
implies: P 
Q,
and: P 
Q,
iff: P 
Q,
rev_implies: P Q,
so_lambda: 
x.t[x],
member: t 
T,
dataflow-equiv: d1 d2,
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
subtype: S 
T,
top: Top,
ycomb: Y,
length: ||as||,
prop: 
,
pi1: fst(t),
pi2: snd(t),
let: let,
true: True,
squash: 
T,
so_lambda: x y.t[x; y],
nat: ,
tl: tl(l),
hd: hd(l),
so_apply: x[s1;s2]
Lemmas :
better-feedback-data-stream,
nat_wf,
dataflow_wf,
bool_wf,
dataflow-equiv_wf,
int_seg_wf,
all_wf,
feedback-dataflow-equiv,
parallel-dataflow_functionality,
parallel-dataflow_wf,
data-stream-cons,
top_wf,
tl_wf,
length_wf,
ge_wf,
hd_wf,
equal_wf,
and_wf,
dataflow-ap_wf,
true_wf,
squash_wf,
ifthenelse_wf,
rec-dataflow_wf,
data-stream_wf
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C {}\mrightarrow{} C].
\mforall{}[ds1,ds2:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[buf:C]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}].
better-feedback-dataflow(n;ds1;F;buf;x.P[x]) \mequiv{} better-feedback-dataflow(n;ds2;F;buf;x.P[x])
supposing \mforall{}k:\mBbbN{}n. ds1 k \mequiv{} ds2 k
Date html generated:
2012_01_23-AM-11_58_04
Last ObjectModification:
2011_12_13-AM-10_34_49
Home
Index