{ 
[cr:CompilationResult]. comp-spec(cr) 
EO' 
' supposing comp-wf(cr) }
{ Proof }
Definitions occuring in Statement :
comp-spec: comp-spec(cr),
comp-wf: comp-wf(cr),
compilation-result: CompilationResult,
Message: Message,
event-ordering+: EO+(Info),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
comp-wf: comp-wf(cr),
member: t T,
prop: ,
comp-spec: comp-spec(cr),
pi1: fst(t),
pi2: snd(t),
top: Top,
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
all: x:A. B[x],
implies: P 
Q,
subtype: S 
T,
compilation-result: CompilationResult,
so_apply: x[s1;s2],
so_apply: x[s]
Lemmas :
pi1_wf_top,
event-ordering+_wf,
Message_wf,
InitSys_wf,
strong-realizes_wf,
std-n2m_wf,
std-l2m_wf,
reliable-env_wf2,
RunType_wf,
EnvType_wf,
comp-wf_wf,
compilation-result_wf
\mforall{}[cr:CompilationResult]. comp-spec(cr) \mmember{} EO' {}\mrightarrow{} \mBbbP{}' supposing comp-wf(cr)
Date html generated:
2011_08_17-PM-04_37_23
Last ObjectModification:
2011_06_18-AM-11_48_26
Home
Index