Nuprl Lemma : dataflow-to-Process_wf
[A,B:Type]. [F:dataflow(A;B)]. [g:B 
LabeledDAG(Id 
(Com(P.A) Process(P.A)))].
(dataflow-to-Process(
F;
g) 
Process(P.A))
Proof not projected
Definitions occuring in Statement :
dataflow-to-Process: dataflow-to-Process,
Process: Process(P.M[P]),
Com: Com(P.M[P]),
ldag: LabeledDAG(T),
dataflow: dataflow(A;B),
Id: Id,
uall: [x:A]. B[x],
member: t T,
apply: f a,
function: x:A B[x],
product: x:A B[x],
universe: Type
Definitions :
implies: P 
Q,
all: x:A. B[x],
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
dataflow-to-Process: dataflow-to-Process,
member: t T,
uall: [x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
uimplies: b supposing a
Lemmas :
Id_wf,
ldag_wf,
Com_wf,
Com-subtype,
subtype_rel_self,
subtype_rel_simple_product,
Process_wf,
subtype_rel-ldag,
dataflow-ap_wf,
continuous-constant,
dataflow_wf,
rec-process_wf_Process
\mforall{}[A,B:Type]. \mforall{}[F:dataflow(A;B)]. \mforall{}[g:B {}\mrightarrow{} LabeledDAG(Id \mtimes{} (Com(P.A) Process(P.A)))].
(dataflow-to-Process(
F;
g) \mmember{} Process(P.A))
Date html generated:
2012_01_23-PM-12_41_43
Last ObjectModification:
2011_12_14-PM-11_31_42
Home
Index