Nuprl Lemma : feedback-prog_wf
[A:{A:
'| 
A} ]. [dfps:DataflowProgram(A) List]. [B:{B:Type| valueall-type(B)} ].
[G:tuple-type(map(
dfp.bag(df-program-type(dfp));dfps)) 
bag(B) bag(B)].
[halt:tuple-type(map(dfp.(Top?);dfps)) 
]. [init:bag(B)].
(G|dfps|
feedback: init
halt: halt 
DataflowProgram(A))
Proof not projected
Definitions occuring in Statement :
feedback-prog: feedback-prog,
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
map: map(f;as),
bool: ,
uall: [x:A]. B[x],
top: Top,
squash: T,
unit: Unit,
member: t T,
set: {x:A| B[x]} ,
lambda: x.A[x],
function: x:A B[x],
union: left + right,
list: type List,
universe: Type,
bag: bag(T),
tuple-type: tuple-type(L),
valueall-type: valueall-type(T)
Definitions :
false: False,
not: 
A,
prop: 
,
le: A 
B,
and: P 
Q,
lelt: i j < k,
subtype: S 
T,
int_seg: {i..j
},
so_lambda: 
x.t[x],
all: x:A. B[x],
implies: P 
Q,
feedback-prog: feedback-prog,
member: t T,
unit: Unit,
top: Top,
dataflow-program: DataflowProgram(A),
uall: [x:A]. B[x],
pi2: snd(t),
pi1: fst(t),
spreadn: spread4,
df-program-statetype: df-program-statetype(dfp),
df-program-type: df-program-type(dfp),
bfalse: ff,
btrue: tt,
exposed-bfalse: exposed-bfalse,
has-valueall: has-valueall(a),
ifthenelse: if b then t else f fi ,
true: True,
squash: T,
ycomb: Y,
zip: zip(as;bs),
map: map(f;as),
nat: 
,
uimplies: b supposing a,
so_apply: x[s],
uiff: uiff(P;Q),
bool: ,
has-value: has-value(a),
it: 
Lemmas :
less_than_wf,
nat_wf,
equal_wf,
and_wf,
length-map,
squash_wf,
df-program-type_wf,
bool_wf,
int_inc_real,
real-has-value,
int_seg_wf,
map_length,
length_wf_nat,
non_neg_length,
select_wf,
df-program-state_wf,
length_wf,
lelt_wf,
top_wf,
select-map,
tuple_wf,
bag-valueall-type,
equal-valueall-type,
df-program-statetype-valueall-type,
union-valueall-type,
tuple-type-valueall-type,
product-valueall-type,
bag_wf,
unit_wf2,
df-program-statetype_wf,
dataflow-program_wf,
map_wf,
tuple-type_wf,
valueall-type_wf,
subtype_rel_bag,
subtype_rel_self,
subtype_rel_simple_product,
empty-bag_wf,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
assert_wf,
uiff_transitivity,
it_wf,
eqtt_to_assert,
function-valueall-type,
subtype_rel_sum,
subtype_rel_tuple-type,
ap2-tuple_wf,
zip_wf,
pi2_wf,
pi1_wf_top,
subtype_rel-equal,
true_wf,
df-program-type-valueall-type,
map-tuple_wf,
bag-subtype-list,
null_wf3,
evalall_wf
\mforall{}[A:\{A:\mBbbU{}'| \mdownarrow{}A\} ]. \mforall{}[dfps:DataflowProgram(A) List]. \mforall{}[B:\{B:Type| valueall-type(B)\} ].
\mforall{}[G:tuple-type(map(\mlambda{}dfp.bag(df-program-type(dfp));dfps)) {}\mrightarrow{} bag(B) {}\mrightarrow{} bag(B)].
\mforall{}[halt:tuple-type(map(\mlambda{}dfp.(Top?);dfps)) {}\mrightarrow{} \mBbbB{}]. \mforall{}[init:bag(B)].
(G|dfps|
feedback: init
halt: halt \mmember{} DataflowProgram(A))
Date html generated:
2012_01_23-AM-11_59_21
Last ObjectModification:
2011_12_14-PM-05_29_45
Home
Index