{ 
[Info:
']. (eclass-program{i:l}(Info) 
') }
{ Proof }
Definitions occuring in Statement :
eclass-program: eclass-program{i:l}(Info),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
eclass-program: eclass-program{i:l}(Info),
so_lambda: 
x.t[x],
so_apply: x[s]
Lemmas :
fpf_wf,
Id_wf,
dataflow-program_wf,
df-program-type_wf,
top_wf
\mforall{}[Info:\mBbbU{}']. (eclass-program\{i:l\}(Info) \mmember{} \mBbbU{}')
Date html generated:
2011_08_16-PM-06_13_36
Last ObjectModification:
2011_06_20-AM-01_50_56
Home
Index