Nuprl Lemma : local-simulation-agreement

∀correct:Id ─→ ℙ. ∀g,f:Name ─→ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀R:Interface ─→ Interface ─→ ℙ. ∀es:EO+(Message(f)).
          ((∀i,j:Id.  ((correct i) ⇒ (correct j) ⇒ local-simulation-input-consistency(g;X;hdr;locs;es;i;j)))
          ⇒ (∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀eo:EO+(Message(g)). (eo-msg-interface-constraint(eo;X;hdrs;g) ⇒ any v1,v2 from X satisfy R[v1;v2]))
          ⇒ any v1,v2 from local-simulation-class(X;locs;hdr) satisfy
             R[v1;v2]
             at locations i.correct i) 
        supposing hdr encodes Id × Message(g)))


Proof



Definitions occuring in Statement :  local-simulation-input-consistency: local-simulation-input-consistency(g;X;hdr;locs;es;i;j),  local-simulation-input-validity: local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i),  eo-msg-interface-constraint: eo-msg-interface-constraint(es;X;hdrs;f),  msg-interface: Interface,  local-simulation-class: local-simulation-class(X;locs;hdr),  encodes-msg-type: hdr encodes T,  Message: Message(f),  local-class: LocalClass(X),  correct-consistent-class: correct-consistent-class,  consistent-class: consistent-class,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  Id: Id,  name: Name,  list: T List,  uimplies: b supposing a,  prop: ℙ,  so_apply: x[s1;s2],  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a,  function: x:A ─→ B[x],  product: x:A × B[x],  universe: Type,  bag: bag(T)
Lemmas :  l_all_cons,  es-E_wf,  event-ordering+_subtype,  Message_wf,  eo-msg-interface-constraint_wf,  local-simulation-eo_wf,  cons_wf,  nil_wf,  local-simulation-msg-constraint,  es-loc_wf,  l_all_single,  uall_wf,  msg-interface_wf,  isect_wf,  classrel_wf,  local-simulation-class_wf,  assert_wf,  has-header-and-in-locs_wf,  es-info_wf,  subtype_rel_product,  Id_wf,  top_wf,  subtype_top,  subtype_rel_transitivity,  exists_wf
Latex:
\mforall{}correct:Id  {}\mrightarrow{}  \mBbbP{}.  \mforall{}g,f:Name  {}\mrightarrow{}  Type.  \mforall{}X:EClass(Interface).
    (LocalClass(X)
    {}\mRightarrow{}  (\mforall{}locs:bag(Id).  \mforall{}hdr:Name.
                \mforall{}hdrs:Name  List.  \mforall{}R:Interface  {}\mrightarrow{}  Interface  {}\mrightarrow{}  \mBbbP{}.  \mforall{}es:EO+(Message(f)).
                    ((\mforall{}i,j:Id.
                            ((correct  i)
                            {}\mRightarrow{}  (correct  j)
                            {}\mRightarrow{}  local-simulation-input-consistency(g;X;hdr;locs;es;i;j)))
                    {}\mRightarrow{}  (\mforall{}i:Id.  ((correct  i)  {}\mRightarrow{}  local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
                    {}\mRightarrow{}  (\mforall{}eo:EO+(Message(g))
                                (eo-msg-interface-constraint(eo;X;hdrs;g)  {}\mRightarrow{}  any  v1,v2  from  X  satisfy  R[v1;v2]))
                    {}\mRightarrow{}  any  v1,v2  from  local-simulation-class(X;locs;hdr)  satisfy
                          R[v1;v2]
                          at  locations  i.correct  i) 
                supposing  hdr  encodes  Id  \mtimes{}  Message(g)))


Date html generated: 2015_07_22-PM-00_07_08
Last ObjectModification: 2015_01_28-AM-11_42_55

Home Index