---

CompilationResult ==
  wf:'  (x:wf
             (spec:EO+(Message)  '  {sys:InitSys| 
                                         assuming(env,r.reliable-env(env; r))
                                          sys |= es.spec es} ))

---

Definitions :  isect: x:A. B[x],  product: x:A  B[x],  function: x:A  B[x],  event-ordering+: EO+(Info),  Message: Message,  prop: ,  set: {x:A| B[x]} ,  InitSys: InitSys,  strong-realizes: strong-realizes,  std-n2m: std-n2m(),  std-l2m: std-l2m(),  reliable-env: reliable-env(env; r),  apply: f a
FDL editor aliases :  compilation-result

---

CompilationResult  ==
    wf:\mBbbP{}'  \mtimes{}  (\mcap{}x:wf
                          (spec:EO+(Message)  {}\mrightarrow{}  \mBbbP{}'  \mtimes{}  \{sys:InitSys| 
                                                                                  assuming(env,r.reliable-env(env;  r))
                                                                                    sys  |=  es.spec  es\}  ))


Date html generated: 2010_08_27-PM-08_22_26
Last ObjectModification: 2010_06_23-AM-11_09_10

Home Index