Nuprl Lemma : parallel-df-program-type
[A:
']. [dfps:DataflowProgram(A) List].
[B:Type]. [F:Top]. (df-program-type(parallel-df-program(B;F;dfps)) = B) supposing 0 < ||dfps||
Proof not projected
Definitions occuring in Statement :
parallel-df-program: parallel-df-program(B;F;dfps),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
length: ||as||,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
less_than: a < b,
list: type List,
natural_number: $n,
universe: Type,
equal: s = t
Definitions :
nat: 
,
ge: i 
j ,
false: False,
not: 
A,
le: A 
B,
uall: [x:A]. B[x],
uimplies: b supposing a,
parallel-df-program: parallel-df-program(B;F;dfps),
member: t 
T,
all: x:A. B[x],
implies: P 
Q,
guard: {T},
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
top: Top,
hd: hd(l),
tl: tl(l),
length: ||as||,
true: True,
squash: 
T,
pi1: fst(t),
df-program-type: df-program-type(dfp),
spreadn: spread4,
parallel-df-prog2: parallel-df-prog2(B;G;dfp1;dfp2),
subtype: S 
T,
parallel-df-prog1: parallel-df-prog1(B;G;dfp),
prop: 
,
bool: 
,
unit: Unit,
uiff: uiff(P;Q),
and: P 
Q,
sq_stable: SqStable(P),
dataflow-program: DataflowProgram(A),
it: 
Lemmas :
ge_wf,
nat_properties,
nat_wf,
length_wf_nat,
length_wf,
dataflow-program_wf,
top_wf,
less_than_wf,
le_wf,
lt_int_wf,
bool_wf,
uiff_transitivity,
equal_wf,
assert_wf,
eqtt_to_assert,
assert_of_lt_int,
le_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
eq_int_wf,
assert_of_eq_int,
not_wf,
assert_of_bnot,
not_functionality_wrt_uiff,
bag_wf,
bag-merge_wf,
df-program-type_wf,
tl_wf,
hd_wf,
parallel-df-prog2_wf,
sq_stable__valueall-type,
union-valueall-type,
non_neg_length
\mforall{}[A:\mBbbU{}']. \mforall{}[dfps:DataflowProgram(A) List].
\mforall{}[B:Type]. \mforall{}[F:Top]. (df-program-type(parallel-df-program(B;F;dfps)) = B) supposing 0 < ||dfps||
Date html generated:
2012_01_23-PM-12_00_29
Last ObjectModification:
2011_12_18-AM-09_15_18
Home
Index