{ 
[M:Type 
Type]
[info:pRunInfo(P.M[P])]
(norm-runinfo(info) 
{info':pRunInfo(P.M[P])| info' = info} )
supposing P:Type. value-type(M[P]) }
{ Proof }
Definitions occuring in Statement :
norm-runinfo: norm-runinfo(info),
pRunInfo: pRunInfo(P.M[P]),
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type,
equal: s = t,
value-type: value-type(T)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
all: x:A. B[x],
so_apply: x[s],
member: t T,
norm-runinfo: norm-runinfo(info),
so_lambda: 
x.t[x],
pRunInfo: pRunInfo(P.M[P]),
spreadn: spread3,
has-value: has-value(a),
pMsg: pMsg(P.M[P]),
unit: Unit,
subtype: S 
T,
it: 
,
guard: {T}
Lemmas :
pRunInfo_wf,
value-type_wf,
Id-has-value,
rational-has-value,
int_inc,
Process_wf,
unit_wf,
Id_wf,
pMsg_wf,
it_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[info:pRunInfo(P.M[P])]. (norm-runinfo(info) \mmember{} \{info':pRunInfo(P.M[P])| info' = info\} )
supposing \mforall{}P:Type. value-type(M[P])
Date html generated:
2011_08_16-PM-06_54_35
Last ObjectModification:
2011_06_18-AM-11_09_32
Home
Index