{ 
[n:Top]. [inputs:Top List]. (null-process(n)*(inputs) ~ null-process(n)) }
{ Proof }
Definitions occuring in Statement :
null-process: null-process(n),
iterate-dataflow: P*(inputs),
uall: [x:A]. B[x],
top: Top,
list: type List,
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
member: t 
T,
null-process: null-process(n),
pi1: fst(t),
rec-process: RecProcess(s0;s,m.next[s; m])
Lemmas :
top_wf
\mforall{}[n:Top]. \mforall{}[inputs:Top List]. (null-process(n)*(inputs) \msim{} null-process(n))
Date html generated:
2011_08_16-AM-09_53_56
Last ObjectModification:
2011_06_18-AM-08_36_07
Home
Index