{ 
[M:Type 
Type]. [n:
].
lvprocess(lp.M[lp];n) 
input(lp.M[lp];n)
(lvprocess(lp.M[lp];n) 
((Id process-input'(lp.M[lp];n)) List)) }
{ Proof }
Definitions occuring in Statement :
process-input': process-input'(lp.M[lp];n),
process-input: input(lp.M[lp];n),
lvprocess: lvprocess(lp.M[lp];n),
Id: Id,
ext-eq: A B,
nat: ,
uall: [x:A]. B[x],
so_apply: x[s],
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
nat: ,
ext-eq: A B,
lvprocess: lvprocess(lp.M[lp];n),
so_apply: x[s],
process-input: input(lp.M[lp];n),
process-input': process-input'(lp.M[lp];n),
member: t 
T,
so_lambda: 
x.t[x],
squash: 
T,
true: True,
ycomb: Y,
and: P 
Q,
prop: 
,
int_seg: {i..j
},
lelt: i 
j < k
Lemmas :
dataflow-ext-eq,
process-input_wf,
Id_wf,
process-input'_wf,
ext-eq_wf,
squash_wf,
true_wf,
dataflow_wf,
nat_wf,
ifthenelse_wf,
le_int_wf,
top_wf,
lvprocess_wf,
int_seg_wf,
le_wf
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[n:\mBbbN{}].
lvprocess(lp.M[lp];n) \mequiv{} input(lp.M[lp];n)
{}\mrightarrow{} (lvprocess(lp.M[lp];n) \mtimes{} ((Id \mtimes{} process-input'(lp.M[lp];n)) List))
Date html generated:
2011_08_17-PM-06_37_20
Last ObjectModification:
2011_06_18-PM-12_01_07
Home
Index