---

{ [es:EO']. [e:E]. [T:Type]. [v:T]. [hdr:Name].
    (make-Msg(hdr;T;v) = info(e)) supposing 
       ((es-header(es;e) = hdr) and 
       (msg-body(info(e)) = v) and 
       (msg-type(info(e)) == T) and 
       valueall-type(T)) }

{ Proof }

---

Definitions occuring in Statement :  make-Msg: make-Msg(hdr;typ;val),  es-header: es-header(es;e),  msg-type: msg-type(msg),  msg-body: msg-body(msg),  Message: Message,  es-info: info(e),  event-ordering+: EO+(Info),  es-E: E,  name: Name,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  universe: Type,  equal: s = t,  valueall-type: valueall-type(T),  eq_term: a == b
Lemmas :  sq_stable__equal,  sq_stable__all,  squash_wf,  subtype_base_sq,  make-Msg_wf,  uiff_wf,  assert-name_eq,  assert-eq_term,  msg-body_wf2,  es-info_wf,  Message_wf,  true_wf,  msg-has-type_wf,  ifthenelse_wf,  false_wf,  assert_wf,  subtype_rel_wf,  intensional-universe_wf,  member_wf,  es-header_wf,  name_wf,  valueall-type_wf,  es-E_wf,  event-ordering+_wf,  uall_wf,  msg-body_wf,  eq_term_wf,  msg-type_wf,  unit_wf,  bool_wf,  type-valueall-type,  es-base-E_wf,  subtype_rel_self,  event-ordering+_inc

---

\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[T:Type].  \mforall{}[v:T].  \mforall{}[hdr:Name].
    (make-Msg(hdr;T;v)  =  info(e))  supposing 
          ((es-header(es;e)  =  hdr)  and 
          (msg-body(info(e))  =  v)  and 
          (\muparrow{}msg-type(info(e))  ==  T)  and 
          valueall-type(T))


Date html generated: 2011_08_17-PM-04_07_46
Last ObjectModification: 2011_07_22-PM-12_59_08

Home Index