Nuprl Lemma : df-program-transition_wf
[Info:Type]. [dfp:DataflowProgram(Info)].
(df-program-transition(dfp) 
df-program-statetype(dfp)
Info
(df-program-statetype(dfp)? 
bag(df-program-type(dfp))))
Proof not projected
Definitions occuring in Statement :
df-program-transition: df-program-transition(dfp),
df-program-statetype: df-program-statetype(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
uall: [x:A]. B[x],
unit: Unit,
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
universe: Type,
bag: bag(T)
Definitions :
pi1: fst(t),
pi2: snd(t),
df-program-transition: df-program-transition(dfp),
df-program-type: df-program-type(dfp),
df-program-statetype: df-program-statetype(dfp),
member: t T,
uall: [x:A]. B[x],
dataflow-program: DataflowProgram(A)
Lemmas :
dataflow-program_wf
\mforall{}[Info:Type]. \mforall{}[dfp:DataflowProgram(Info)].
(df-program-transition(dfp) \mmember{} df-program-statetype(dfp)
{}\mrightarrow{} Info
{}\mrightarrow{} (df-program-statetype(dfp)? \mtimes{} bag(df-program-type(dfp))))
Date html generated:
2012_02_20-PM-02_42_45
Last ObjectModification:
2012_02_08-PM-11_31_48
Home
Index