{ 
[M:Type 
Type]
[m,n:
]. [Ps:n lvprocess(lp.M[lp];m)].
[F:n ((Id 
process-input'(lp.M[lp];m)) List)
((Id process-input'(lp.M[lp];m)) List)].
(parallel-process(Ps;F) 
lvprocess(lp.M[lp];m))
supposing A,B:Type. ((A 
r B) 
(M[A] r M[B])) }
{ Proof }
Definitions occuring in Statement :
parallel-process: parallel-process(Ps;F),
process-input': process-input'(lp.M[lp];n),
lvprocess: lvprocess(lp.M[lp];n),
Id: Id,
subtype_rel: A r B,
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
natural_number: $n,
universe: Type
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
all: x:A. B[x],
implies: P Q,
so_apply: x[s],
nat: ,
lvprocess: lvprocess(lp.M[lp];n),
process-input': process-input'(lp.M[lp];n),
member: t T,
parallel-process: parallel-process(Ps;F),
ycomb: Y,
so_lambda: 
x.t[x],
subtype: S T,
suptype: suptype(S; T),
int_seg: {i..j},
lelt: i 
j < k,
and: P 
Q,
prop: 
Lemmas :
parallel-dataflow_wf,
nat_wf,
ifthenelse_wf,
le_int_wf,
top_wf,
lvprocess_wf,
Id_wf,
int_seg_wf,
le_wf,
process-input'_wf,
dataflow_wf,
nat_properties,
subtype_rel_self,
subtype_rel_list,
subtype_rel_simple_product,
dataflow_subtype
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[m,n:\mBbbN{}]. \mforall{}[Ps:\mBbbN{}n {}\mrightarrow{} lvprocess(lp.M[lp];m)]. \mforall{}[F:\mBbbN{}n {}\mrightarrow{} ((Id \mtimes{} process-input'(lp.M[lp];m)) List)
{}\mrightarrow{} ((Id \mtimes{} process-input'(lp.M[lp];m)) List)].
(parallel-process(Ps;F) \mmember{} lvprocess(lp.M[lp];m))
supposing \mforall{}A,B:Type. ((A \msubseteq{}r B) {}\mRightarrow{} (M[A] \msubseteq{}r M[B]))
Date html generated:
2011_08_17-PM-06_38_48
Last ObjectModification:
2011_06_18-PM-12_04_34
Home
Index