Nuprl Lemma : iterate-better-feedback-dataflow
[A,C:Type]. [n:
]. [B:n 
Type]. [P:C 
]. [F:k:n B[k] C C]. [L:A List].
[ds:k:n dataflow(A;B[k])]. [s:C].
(better-feedback-dataflow(n;ds;F;s;x.P[x])*(L)
= better-feedback-dataflow(n;
k.ds k*(L);
F;let L' = filter(x.P[x];data-stream(better-feedback-dataflow(n;ds;F;s;x.P[x]);L)) in
if null(L') then s else last(L') fi ;x.P[x]))
Proof not projected
Definitions occuring in Statement :
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
data-stream: data-stream(P;L),
iterate-dataflow: P*(inputs),
dataflow: dataflow(A;B),
null: null(as),
ifthenelse: if b then t else f fi ,
bool: ,
int_seg: {i..j
},
nat: ,
let: let,
uall: [x:A]. B[x],
so_apply: x[s],
apply: f a,
lambda: x.A[x],
function: x:A B[x],
list: type List,
natural_number: $n,
universe: Type,
equal: s = t,
filter: filter(P;l),
last: last(L)
Definitions :
reduce: reduce(f;k;as),
member: t 
T,
filter: filter(P;l),
so_apply: x[s],
uall: [x:A]. B[x],
true: True,
squash: 
T,
so_lambda: 
x.t[x],
btrue: tt,
null: null(as),
ifthenelse: if b then t else f fi ,
let: let,
all: x:A. B[x],
so_lambda: x y.t[x; y],
subtype: S 
T,
top: Top,
pi2: snd(t),
pi1: fst(t),
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
guard: {T},
bfalse: ff,
and: P 
Q,
implies: P 
Q,
iff: P 
Q,
rev_implies: P Q,
not: 
A,
prop: 
,
assert: 
b,
nat: ,
so_apply: x[s1;s2],
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
unit: Unit,
bool: ,
false: False,
it: 
Lemmas :
nat_wf,
bool_wf,
dataflow_wf,
int_seg_wf,
true_wf,
squash_wf,
better-feedback-dataflow_wf,
eval-parallel-dataflow_wf,
rec-dataflow_wf,
ifthenelse_wf,
equal_wf,
dataflow-ap_wf,
eval-parallel-dataflow-property,
top_wf,
data-stream-cons,
last_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
assert_of_null,
assert_wf,
uiff_transitivity,
null_wf3,
data-stream_wf,
filter_wf,
iterate-dataflow_wf,
eqtt_to_assert,
dataflow-out_wf,
pi1_wf_top,
false_wf,
nat_properties,
last-cons,
iff_weakening_uiff,
pi2_wf
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[L:A List].
\mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[s:C].
(better-feedback-dataflow(n;ds;F;s;x.P[x])*(L)
= better-feedback-dataflow(n;\mlambda{}k.ds k*(L);
F;let L' = filter(\mlambda{}x.P[x];data-stream(better-feedback-dataflow(n;ds;F;s;x.P[x]);L)) in
if null(L') then s else last(L') fi ;x.P[x]))
Date html generated:
2012_01_23-AM-11_57_09
Last ObjectModification:
2011_12_14-PM-04_14_42
Home
Index