---

{ [cr:CompilationResult]
    comp-system(cr)  {sys:InitSys| 
                       assuming(env,r.reliable-env(env; r))
                        sys |= es.comp-spec(cr) es}  
    supposing comp-wf(cr) }

{ Proof }

---

Definitions occuring in Statement :  comp-system: comp-system(cr),  comp-spec: comp-spec(cr),  comp-wf: comp-wf(cr),  compilation-result: CompilationResult,  std-l2m: std-l2m(),  std-n2m: std-n2m(),  strong-realizes: strong-realizes,  InitSys: InitSys,  reliable-env: reliable-env(env; r),  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T,  set: {x:A| B[x]} ,  apply: f a
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  comp-wf: comp-wf(cr),  member: t  T,  comp-spec: comp-spec(cr),  comp-system: comp-system(cr),  prop: ,  pi1: fst(t),  pi2: snd(t),  so_lambda: x y.t[x; y],  so_lambda: x.t[x],  all: x:A. B[x],  implies: P  Q,  compilation-result: CompilationResult,  so_apply: x[s1;s2],  so_apply: x[s]
Lemmas :  event-ordering+_wf,  Message_wf,  InitSys_wf,  strong-realizes_wf,  std-n2m_wf,  std-l2m_wf,  reliable-env_wf2,  RunType_wf,  EnvType_wf,  pi2_wf,  comp-wf_wf,  compilation-result_wf

---

\mforall{}[cr:CompilationResult]
    comp-system(cr)  \mmember{}  \{sys:InitSys|  assuming(env,r.reliable-env(env;  r))  sys  |=  es.comp-spec(cr)  es\}   
    supposing  comp-wf(cr)


Date html generated: 2011_08_17-PM-04_37_33
Last ObjectModification: 2011_06_18-AM-11_48_39

Home Index