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